Théo Zimmermann (Aug 08 2020 at 10:07): Théo Zimmermann (Aug 08 2020 at 10:07):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
Bas Spitters (Aug 08 2020 at 10:22):How about the slides?
Karl Palmskog (Aug 08 2020 at 13:26):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
Karl Palmskog (Aug 08 2020 at 13:29):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...
Théo Zimmermann (Aug 09 2020 at 06:06):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.
Théo Zimmermann (Aug 09 2020 at 06:09):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.
Rob Lewis (Aug 09 2020 at 10:17):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
Utensil Song (Aug 12 2020 at 07:22):Bas Spitters said:
How about the slides?
http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/ug_maths.pdf
Bas Spitters (Aug 12 2020 at 09:18):@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.
Bas Spitters (Aug 12 2020 at 10:21):@Théo Zimmermann What did you take away from the talk?
Théo Zimmermann (Aug 12 2020 at 11:43):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.
Théo Zimmermann (Aug 12 2020 at 11:45):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.
Michael Soegtrop (Aug 12 2020 at 13:43):A few thoughts from my side:
Karl Palmskog (Aug 12 2020 at 13:46):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
Bas Spitters (Aug 12 2020 at 13:52):@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
Karl Palmskog (Aug 12 2020 at 13:52):yes, I'm familiar with that approach, and I think it's something that the Coq community should avoid
Karl Palmskog (Aug 12 2020 at 13:53):there is basically no way of telling whether an abstract is correctly formalized (proofs are the "tests" for definitions/statements)
Bas Spitters (Aug 12 2020 at 13:58):@Karl Palmskog I'm curious about the meta-issue. I think it all ties up with the platform/stdlib2 discussion.
Karl Palmskog (Aug 12 2020 at 13:59):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.
Bas Spitters (Aug 12 2020 at 14:02):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?).
Théo Zimmermann (Aug 12 2020 at 14:03):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.
Bas Spitters (Aug 12 2020 at 14:05):But they would fit in the platform?
Théo Zimmermann (Aug 12 2020 at 14:06):Definitely! But not right from the start: platform stuff is supposed to be relatively stable stuff.
Bas Spitters (Aug 12 2020 at 14:38):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.
Anton Trunov (Aug 12 2020 at 15:19):@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
Bas Spitters (Aug 12 2020 at 15:37):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 (?)
Karl Palmskog (Aug 14 2020 at 17:57):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) Bas Spitters (Aug 14 2020 at 18:23):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
Karl Palmskog (Aug 14 2020 at 18:27):they have a lot of stuff at Marelle at different servers (and they are accessible with some effort in latest browsers, just not trivially).
Karl Palmskog (Aug 14 2020 at 18:31):I wrote up the issue now, so I guess we can begin piling on there: https://github.com/coq-community/manifesto/issues/111
Karl Palmskog (Aug 14 2020 at 18:40):unless the transcendental Coq stuff has been integrated somewhere, it is also under threat of extinction when Inria closes gforge :sad:
Bas Spitters (Aug 14 2020 at 18:42):@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.
Karl Palmskog (Aug 14 2020 at 18:43):well, the Lean community is in Monorepo mode, but I wonder for how long?
Karl Palmskog (Aug 14 2020 at 18:44):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 ...
Paolo Giarrusso (Aug 14 2020 at 19:56):also re GForge — any change to get pages copied on the Internet Archive?
Karl Palmskog (Aug 15 2020 at 17:32):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)
Karl Palmskog (Aug 15 2020 at 17:49):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/
Karl Palmskog (Aug 15 2020 at 17:51):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
Karl Palmskog (Aug 15 2020 at 18:06):coincidentally, there is a name clash between Coqtail-the-library and Coqtail-the-VIM-Coq-frontend (https://github.com/whonore/Coqtail)
Wolf Honore (Aug 15 2020 at 18:11):Hm, somehow I missed that when choosing a name. There just aren't enough Coq puns to go around
Karl Palmskog (Aug 15 2020 at 18:50):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).
Jalex Stark (Aug 17 2020 at 22:41):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
Since the community's growth is largely driven by mathematicians, the demand for metaprogramming and dev tools outsrips the supply by a lot.
Karl Palmskog (Aug 17 2020 at 23:03):@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.)
Karl Palmskog (Aug 17 2020 at 23:07):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!".
Jalex Stark (Aug 18 2020 at 01:32):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.
Théo Zimmermann (Aug 18 2020 at 15:59):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.
Jalex Stark (Aug 19 2020 at 02:17):Wow, your thesis seems very nice.
Karl Palmskog (Aug 27 2020 at 09:10):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
Karl Palmskog (Aug 27 2020 at 09:12):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.
Rob Lewis (Aug 27 2020 at 09:34):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.
Karl Palmskog (Aug 27 2020 at 09:43):@Rob Lewis but wouldn't it make sense to have an "official" goal then, e.g., one that at least maintainers agree on?
Rob Lewis (Aug 27 2020 at 09:49):No, I'm not sure having an "official" goal is necessary, at least right now.
Michael Soegtrop (Aug 27 2020 at 10:25):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.
Karl Palmskog (Aug 27 2020 at 10:30):@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.
Karl Palmskog (Aug 27 2020 at 10:31):for Coq I totally I agree this would be infeasible, but we are probably the furthest from a monorepo assumption of all proof assistants
Karl Palmskog (Sep 11 2020 at 17:55):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)
Karl Palmskog (Sep 11 2020 at 17:57):although I have to confess Coq code in French is a bit harder to read than usual :wink:
Paolo Giarrusso (Sep 11 2020 at 17:59):(deleted)
Last updated: Sep 15 2024 at 12:01 UTC