Yong Kiam (Mar 28 2024 at 15:10): Yong Kiam (Mar 28 2024 at 15:10):This is perhaps an open-ended question, but the "100 theorems" here: https://www.cs.ru.nl/~freek/100/ have pretty much all been formalized (the sole exception is Fermat's last theorem, which I've heard is quite involved :upside_down: ).
Does anyone know of any effort aimed at making a successor to this list?
Wenda Li (Mar 28 2024 at 19:45):There have been some discussions on the Lean zulipchat, where Knill's list appears to be the one that fits the expectation of many of the Lean users (i.e., working mathematicians).
Yong Kiam (Mar 28 2024 at 23:58):thanks for the pointer, this is a nice list indeed
Manuel Eberl (Mar 29 2024 at 10:22):I went through the list and I believe we have roughly 57 of these 172 theorems. Perhaps a few more.
Yong Kiam (Mar 29 2024 at 10:36):do you mean 272? (I also see the number 172 in the Lean zulip and I'm wondering where that comes from... maybe it includes the original 100 as a subset?)
Manuel Eberl (Mar 29 2024 at 10:55):I used the YAML that one of the Lean people created from the PDF.
Manuel Eberl (Mar 29 2024 at 10:55):I didn't check whether it matches the PDF.
Manuel Eberl (Mar 29 2024 at 10:55):There's some overlap between the YAML and the 100 Theorems list, so I don't think it's a subset.
Yong Kiam (Mar 29 2024 at 10:56):ah, it looks like the 172 was an old number and the pdf was indeed updated to have 272 theorems now
Manuel Eberl (Mar 29 2024 at 10:57):I see.
Last updated: Dec 21 2024 at 12:33 UTC