Stream: Miscellaneous

Topic: Formalizing undergraduate mathematics


view this post on Zulip 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

view this post on Zulip Bas Spitters (Aug 08 2020 at 10:22):

How about the slides?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Aug 12 2020 at 10:21):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Aug 12 2020 at 13:43):

A few thoughts from my side:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?).

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Aug 12 2020 at 14:05):

But they would fit in the platform?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 (?)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Aug 14 2020 at 18:43):

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

view this post on Zulip 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 ...

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 19:56):

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

view this post on Zulip 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)

view this post on Zulip 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/

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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!".

view this post on Zulip 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.

view this post on Zulip 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

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.

view this post on Zulip Jalex Stark (Aug 19 2020 at 02:17):

Wow, your thesis seems very nice.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Rob Lewis (Aug 27 2020 at 09:49):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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:

view this post on Zulip Paolo Giarrusso (Sep 11 2020 at 17:59):

(deleted)


Last updated: Aug 14 2022 at 11:02 UTC