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:

https://github.com/Eelis/hybrid

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:

https://math.unice.fr/%7Ecarlos/themes/verif.html

In case you want it extend it to CS:

https://github.com/EasyCrypt/certicrypt

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:

https://www-sop.inria.fr/marelle/Guillaume.Cano/

These slides tell me that it is now in math-comp analysis.

https://perso.crans.org/cohen/CoqWS2018.pdf

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

About WP4.1

http://coq.io/opam/coq-pi-agm.1.2.6.html

But follow-up work in:

https://www-sop.inria.fr/marelle/distant-decimals-pi/

https://github.com/thery/Plouffe

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: May 18 2024 at 10:02 UTC