List of disused formalized mathematics in Coq

List of disused formalized mathematics in Coq

A lot of mathematics has been formalized in Coq, but unless it ends up in a maintained library, 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.

This is an attempt at a list of such disused formalizations of mathematics in Coq. The hope is that it will lead to better preservation and maintainance of such code. See also the corresponding coq-community issue.

• Proofs of transcendence for e and pi, and Lindemann-Weierstrass theorem (2015): paper 1, paper 2, code
• Certificates for Gröbner bases: code, paper
• Homology and Persistent Homology: code, paper
• Dynamic logic of common knowledge (2007): paper, file, file
• Infinite extensive games (2011): paper, code
• Admissible discrete vector fields: code, paper