A lot of mathematics has been formalized in Coq, but unless it ends up in a bigger library such as 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 a first step to address this problem, I have started to list links to Coq code and corresponding papers for math that is:
- not working with latest stable Coq, and
- not currently maintained.
If someone “proves” me wrong about any of these points for some list entry, all the better.
The list is currently a coq-community wiki page, but could be migrated to a regular GitHub repository if there is interest. See also the corresponding coq-community issue.
Finally, @MSoegtropIMC has suggested that standalone results of Coq mathematics not available in bigger libraries could be maintained in a Coq project/package dedicated to this purpose, tentatively called the “Coq Umbrella Library”.
Feel free to add new entries to the list, and let us know how you think the Coq mathematical community should solve this problem (of leftover results).