search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Listing and preserving formalized mathematical results in Coq #111

Open palmskog opened 3 years ago

palmskog commented 3 years ago

This is a meta issue asking the general question:

How can coq-community work towards better listing and preservation of formalized mathematics in Coq?

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:

  1. Organize and maintain a curated list of mathematical results that are available for the latest stable Coq version (an inverse of a list of projects formalizing mathematics such as this one)
  2. Actively locate and port old code with noteworthy math results to the latest stable Coq version, and maintain it on GitHub.

One source of inspiration is what the Lean community is doing:

palmskog commented 3 years ago

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

Casteran commented 3 years ago

I would like to include goedel (and its helper pocklington) contrib in the list. The current version available in coq-contribs is for Coq8.10. The first incompatibilities I noticed were : use of sigS (can be replaced with sigT), and name changes for functions, predicates and lemmas statements on Z. I think that Gödel's incompleteness theorems are of a great pedagogical interest. Also, I would like to import Russel O'Connor's formalization of PR functions, which is part of goedel

palmskog commented 3 years ago

@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.