3
I Use This!
Activity Not Available

Project Summary

The object of this project is to demonstrate that formalized mathematical theories can, like modern software, be built out of components. By components we mean modules that comprise both the static (objects and facts) and dynamic (proof and computation methods) contents of theories. We propose to develop a general platform for mathematical components, based on the Coq “Ssreflect” extension that was used to carry out the formalization of the Four Colour Theorem. We would validate the platform on two significant developments: a theory of efficient arithmetic, and the proof of the Odd Order theorem. The former could be used in the resolution of several outstanding computer proof challenges, among them the Kepler Conjecture, and the latter could become the first step in a new major challenge:

Tags

coq mathematics

In a Nutshell, SSReflect...

 No code available to analyze

Open Hub computes statistics on FOSS projects by examining source code and commit history in source code management systems. This project has no code locations, and so Open Hub cannot perform this analysis

Is this project's source code hosted in a publicly available repository? Do you know the URL? If you do, click the button below and tell us so that Open Hub can generate statistics! It's fast and easy - try it and see!

Add a code location

CeCILL-B Free Software License Agreement
Permitted
Forbidden
Required

These details are provided for information only. No information here is legal advice and should not be used as such.

This Project has No vulnerabilities Reported Against it

Did You Know...

  • ...
    there are over 3,000 projects on the Open Hub with security vulnerabilities reported against them
  • ...
    you can embed statistics from Open Hub on your site
  • ...
    use of OSS increased in 65% of companies in 2016
  • ...
    search using multiple tags to find exactly what you need

 No code available to analyze

Open Hub computes statistics on FOSS projects by examining source code and commit history in source code management systems. This project has no code locations, and so Open Hub cannot perform this analysis

Is this project's source code hosted in a publicly available repository? Do you know the URL? If you do, click the button below and tell us so that Open Hub can generate statistics! It's fast and easy - try it and see!

Add a code location

Community Rating

Be the first to rate this project
Click to add your rating
   Spinner
Review this Project!
Sample ohloh analysis