Kevin Buzzard's invited talk at CICM 2020 contained lots of interesting takeaways IMHO. It is now available on YouTube: https://www.youtube.com/watch?v=FDx0nXFQloE

How about the slides?

as we discussed before, I think we should have some open list of "mathematics formalized in Coq". The inverse of this, basically: https://github.com/coq/coq/wiki/List-of-Coq-Math-Projects

things are bitrotting and disappearing left and right. For example, there is the list of Freek's 100 theorems in Coq (https://github.com/coq/coq/wiki/Top100MathematicalTheoremsInCoq) which has tons of dead links. In fact, the Marelle team's whole website (including many of the members' personal websites which contain some results) is unreachable in modern browsers due to a too-old version of SSL...

Bas Spitters said:

How about the slides?

@Kevin Buzzard Are the slides available somewhere public? The link available in Slack is restricted to CICM registered participants.

Karl Palmskog said:

things are bitrotting and disappearing left and right. For example, there is the list of Freek's 100 theorems in Coq (https://github.com/coq/coq/wiki/Top100MathematicalTheoremsInCoq) which has tons of dead links. In fact, the Marelle team's whole website (including many of the members' personal websites which contain some results) is unreachable in modern browsers due to a too-old version of SSL...

What about creating a coq-community project that would import and restate all the major mathematical theorems? This would provide a good picture of which formalizations are kept up-to-date and which need help against bitrot.

The Lean community has been keeping a few (probably too many) of these lists: Freek's 100, undergrad topcis from the French math curriculum, an overview of what's in mathlib right now. These are all generated from yaml files. The undergrad topics in particular could be a good starting point if you want to make this kind of list: https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/undergrad.yaml

Bas Spitters said:

How about the slides?

http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/ug_maths.pdf

@Théo Zimmermann here's a concrete one:

https://github.com/Ekdohibs/coq-proofs/tree/master/Reciprocity

Would you include it in a separate repo, or try to refactor it, say, on top of the stdlib or coq-prime.

@Théo Zimmermann What did you take away from the talk?

Bas Spitters said:

Théo Zimmermann here's a concrete one:

https://github.com/Ekdohibs/coq-proofs/tree/master/Reciprocity

Would you include it in a separate repo, or try to refactor it, say, on top of the stdlib or coq-prime.

Ideally, I would try to find an existing library where it fits (maybe coq-prime) and suggest making a contribution there.

Bas Spitters said:

Théo Zimmermann What did you take away from the talk?

There were lots of insights but unfortunately I couldn't summarize everything because I've not taken notes (although given that the recording is available now, I might watch it again). One thing in particular that I understood from Kevin's talk is that we should compare math libraries not in the number of theorems they prove but mostly in what definitions they provide, and that as long as many definitions of modern maths are missing from most ITPs, we'll have a hard time convincing professional mathematicians to use them.

A few thoughts from my side:

- Engineering uses mostly what is undergraduate math for mathematicians. Formal methods in engineering is important, so is undergraduate math.
- For engineers it is very important if stuff is correct or not.
- Some formalizations mathematicians do in text books are not that useful when it comes to using them in practice - my favorite example are real numbers.
- From my experience with a son who just started to study physics with a bit tough math classes, I would say that one of the largest and most frustrating problem students have with learning math is to learn the right level of detail in a proof - something mathematicians claim to be logical but in the end is just a convention math students have to learn but are not taught. A proof assistant mostly fixes this, and I believe it is actually easier to learn math with Coq than without. There are of cause still nice and not so nice Coq proofs and I think one should also give ratings for clarity for Coq proofs and not just evaluate correctness (which Coq does for us).

I was starting to write up a meta-issue about this coq-community about what we can/should do. Unfortunately, organizing (collecting?) and advertising Coq undergrad math is a growing and seemingly endless task

@Karl Palmskog Organizing math is an active research topic.

Here's an attempt at that, which seems to have stalled:

https://github.com/formalabstracts/formalabstracts

yes, I'm familiar with that approach, and I think it's something that the Coq community should avoid

there is basically no way of telling whether an abstract is correctly formalized (proofs are the "tests" for definitions/statements)

@Karl Palmskog I'm curious about the meta-issue. I think it all ties up with the platform/stdlib2 discussion.

to me it's disparate from stdlib2. The main goal would not be to unify anything (at least not at first), just to collect references to what is already out there. Platform stuff would also be much later.

One could do that by hand (wiki-style), or try to automate it (as in http://helm.cs.unibo.it/library.html, http://mowgli.cs.unibo.it/). The latter approach does not seem to have taken off (yet?).

I also agree that this is a very different issue. According to the Coq developers, the stdlib should provide only basic stuff that everybody needs. Most of the definitions mathematicians need will not fall in that scope.

But they would fit in the platform?

Definitely! But not right from the start: platform stuff is supposed to be relatively stable stuff.

So, stdlib < platform < community < random github repos ?

Andrej suggested the "google model" where one at least has some kind of search engine for the latter. I guess mowgli was trying to do something similar.

@Bas Spitters I guess there should be a centralized package repo (like the curated coq-opam-archive repo) somewhere before 'random github repos' in the `<`

-chain

And UG math would be in all of them.

Moreover, we expect a flow of packages from left to right and right to left, after the stdlib has been reorganized (?)

another example: https://twitter.com/XenaProject/status/1294300889935745025 and http://marelledocsgit.gforge.inria.fr/transcendence.tar.gz / https://arxiv.org/abs/1512.02791 (with better marketing from Coq side perhaps we could get CPP paper citations here: https://jjaassoonn.github.io/transcendental/src/doc/main.pdf)

My MSc student Jujian Zhang has proved transcendence of e in Lean for his MSc project! https://jjaassoonn.github.io/transcendental/ He's even made docs explaining the math eg https://jjaassoonn.github.io/e_transcendence_doc.html . After 20 years of telling MSc students "here's a Springer GTM, go copy it out" this is much more fun

- The Xena Project (@XenaProject)Are the Marelle pages working again? If not, we should ping the people there.

Also, Liouville's theorem was already proved in 2009 by Valetin Blot:

https://valentinblot.org/pro/M1_report.pdf

they have a lot of stuff at Marelle at different servers (and they are accessible with some effort in latest browsers, just not trivially).

I wrote up the issue now, so I guess we can begin piling on there: https://github.com/coq-community/manifesto/issues/111

unless the transcendental Coq stuff has been integrated somewhere, it is also under threat of extinction when Inria closes gforge :sad:

@Karl Palmskog the work in Lean looks very nice. It would be nice to do something similar in Coq.

I guess the reason the google model doesn't work here, is that repos start to bitrot quickly.

well, the Lean community is in Monorepo mode, but I wonder for how long?

the Coq community could do something similar, but would need tons of tooling and automation to get the same effect (across distributed repos and projects). And just training people to use tooling, if it is available, is difficult. Right now we have some pieces like Dune and the Coq bot and the templates and Docker images ...

also re GForge — any change to get pages copied on the Internet Archive?

some content is already on the Archive, but I have no idea how one would request backing up all subdomains/websites when we don't even know all of them (no centralized list, to my knowledge)

Madiot's list is seemingly the most updated one of Wiedijk's 100 theorems for Coq, but even it references quite a lot of code that doesn't compile with modern Coq: https://madiot.fr/coq100/

this has quite a lot of undergraduate math: https://github.com/coqtail/coqtail/ - there was an issue some time ago about coq-community there: https://github.com/coqtail/coqtail/issues/1

coincidentally, there is a name clash between Coqtail-the-library and Coqtail-the-VIM-Coq-frontend (https://github.com/whonore/Coqtail)

Hm, somehow I missed that when choosing a name. There just aren't enough Coq puns to go around

and of course, unless we convince people to put current and past grey literature publications related to math formalizations on permanent archives (arXiv/HAL) the future will likely see more material gone as websites disappear (e.g., researchers retire and universities take their websites offline).

Karl Palmskog said:

well, the Lean community is in Monorepo mode, but I wonder for how long?

There have been recent discussions about how to make it easier to protect repos that depend on mathlib from fading into irrelevance because of breaking mathlib changes. I guess that decreasing the rate of breaking changes would require one of

- spending more time on review (an increasingly taut constraint; mathlib is recruiting contributors faster than reviewers) or
- having better dev tools (to identify breaking changes more efficiently) or
- having better metaprogramming (to maintain more backwards compatibility without adding much complexity to the source)

Since the community's growth is largely driven by mathematicians, the demand for metaprogramming and dev tools outsrips the supply by a lot.

@Jalex Stark my experience from the formal program verification world is that beginners/enthusiasts can be very productive when put to work to prove something that someone else has set up (specification/framework is given), but when they start to formalize concepts on their own, it's very common for them to go on wild goose chases and build complex solutions that are difficult/unfeasible to maintain. For example, I wonder how many beginners would come up with the following definition of path over a type with equality (and corresponding notion of cycle, etc.)

this is why I personally don't believe the "Mathlib model" is something the Coq community should imitate. I think there are other ways to welcome newcomers and let them learn/contribute than saying "start to formalize!".

Sure, I didn't mean to suggest that "grow as fast as possible and hope that our future selves will clean up the mess" is a good strategy for everyone. It introduces a lot of pain, including the problems I mention in my above comment.

Jalex Stark said:

There have been recent discussions about how to make it easier to protect repos that depend on mathlib from fading into irrelevance because of breaking mathlib changes. I guess that decreasing the rate of breaking changes would require one of

- spending more time on review (an increasingly taut constraint; mathlib is recruiting contributors faster than reviewers) or
- having better dev tools (to identify breaking changes more efficiently) or
- having better metaprogramming (to maintain more backwards compatibility without adding much complexity to the source)

Probably more than one of those. In the Coq development team, we have managed to reduce the impact of breaking changes at new releases by a combination of PR reviewing, CI testing a big number of external projects, and a policy of making sure the compatibility breaking changes are documented with proposals for backward-compatible fixes. Our contributing guide and my own PhD thesis explain more about this.

Wow, your thesis seems very nice.

if anyone is still following this, I started a wiki page I call "disused Coq mathematics", this was the least negative word I could think of for stuff that seems important but isn't close to working in latest Coq: https://github.com/coq-community/manifesto/wiki/List-of-disused-formalized-mathematics-in-Coq

also, interesting that lines are being drawn in the sand: Mathlib's goal is to be a "foundation for all of modern pure mathematics". To me, this would exclude a lot (most?) of CS-related applied math.

Karl Palmskog said:

also, interesting that lines are being drawn in the sand: Mathlib's goal is to be a "foundation for all of modern pure mathematics". To me, this would exclude a lot (most?) of CS-related applied math.

I wouldn't read too much into any one person's claim about what the goals of mathlib are. It's a distributed project. Every contributor has a different idea here.

@Rob Lewis but wouldn't it make sense to have an "official" goal then, e.g., one that at least maintainers agree on?

No, I'm not sure having an "official" goal is necessary, at least right now.

I think one should have stability goals, so that people doing derived work relying on such theorems can assume that it will be possible to port their work to later versions of Coq without porting these theorems themselves. The rationale is not that different from the Coq platform project.

@Michael Soegtrop I believe Lean/Mathlib is (almost) using the "monorepo assumption" right now, i.e., the relevant code is always *in* Mathlib, not in an outside repo depending on Mathlib. As long as this assumption is feasible / mostly true, the absence of stability goals will probably not be a major obstacle in themselves.

for Coq I totally I agree this would be infeasible, but we are probably the furthest from a monorepo assumption of all proof assistants

Thanks to Yves Bertot, the community has recovered the Coq proof of Ptolemy's theorem: https://github.com/coq-community/HighSchoolGeometry/pull/4 (see also the paper)

although I have to confess Coq code in French is a bit harder to read than usual :wink:

(deleted)

Last updated: Sep 15 2024 at 12:01 UTC