I can't think of any other way of getting started with collecting bitrotted Coq math than using the coq-community wiki: https://github.com/coq-community/manifesto/wiki/List-of-disused-formalized-mathematics-in-Coq - other suggestions welcome, though
https://github.com/roglo/puiseuxth compiles with 8.11, apparently
This is also bitrotting:
sigh, Madiot's list is out of date
Also the work by Carlos Simson and his group, which is quite close to what Kevin is trying to do:
In case you want it extend it to CS:
CS fits more for "move project" issues
What's the difference between math and CS in this respect?
I think of CS as more holistic, one formalizes a whole program / language, and the program is generally not something known before
if you look in coq-community issues, we already have certicrypt and hybrid issues there. But math results may be just a small part of other projects.
basically I'm not going to put an issue with "move proof that pi is transcendental to coq-community", so second best thing is to list it in wiki
I think Simpson's Coq work is (maybe with some exception) available in the coq-contribs, which I would at least would consider "preserved"
A lot of things in ForMath that appears to fit: https://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ProofExamples
@Cyril Cohen and @Maxime Dénès were involved in this project from Sophia, and may know more.
I lead the Nijmegen part of WP4, corn and math-classes are part of the community.
CoqEAL is still available.
I think WP3 was mostly done in Isabelle. I'd be happy to provide more information, if you think other things are missing.
for precision if Cyril and Maxime see this, we are interested in listing results that may be of interest to researchers that are not currently included in any modern library.
@Bas Spitters do you know what happened to the other stuff in WP4 (if anything happened at all), like "Rohn's theorem, a sketch of Perron-Frobenius, and canonical forms" (https://wiki.portal.chalmers.se/cse/uploads/ForMath/formath-4.3.zip)
@Yves Bertot and his team worked on that. There's quite an extensive PDF report in the zip file you linked.
P-F was the work by:
These slides tell me that it is now in math-comp analysis.
There was also work by Ioana (https://www-sop.inria.fr/marelle/Ioana.Pasca/phd/ https://www-sop.inria.fr/marelle/Ioana.Pasca/publications.html).
Other parts are available in CoqEAL.
I believe some parts have also been subsumed by @Cyril Cohen s work on robotics.
( Incidentally, https://github.com/aa755/ROSCoq by @Abhishek Anand is another fun application of Coq to robotics.)
But follow-up work in:
About WP3, I see quite a bit of the code is actually in Coq. Do you think it's worth following up?
thanks, so it seems the rest of WP4 is indeed covered. I'll take a look at WP3 later this week
Last updated: Feb 05 2023 at 13:02 UTC