-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Listing and preserving formalized mathematical results in Coq #111
Comments
In lieu of a better location, I'm using the following wiki page to list math-related Coq developments that are candidates for preservation: https://github.com/coq-community/manifesto/wiki/List-of-disused-formalized-mathematics-in-Coq |
I would like to include goedel (and its helper pocklington) contrib in the list. |
@Casteran I didn't list any coq-contribs projects since they are not in any risk of disappearing (all code is on GitHub and key people have administrative access to the repositories). However, if you think the Goedel project is of pedagogical interest, I think we should create a coq-community GitHub issue about this and advertise for a new initial maintainer that can port it to modern Coq. |
This is a meta issue asking the general question:
A lot of mathematics has been formalized in Coq, but unless it ends up in a library such Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.
As one example, consider Madiot's list of Coq theorems from Wiedijk's general list. Quite a few of the links in Madiot's list point to Coq code that does not build with the current stable version of Coq.
coq-community members can address this situation in at least two ways:
One source of inspiration is what the Lean community is doing:
The text was updated successfully, but these errors were encountered: