Zulip Chat Archive

Stream: general

Topic: List of formalized proofs for comparing formal proof systems

Mario Krenn (Jun 22 2021 at 13:49):

Hi! Sorry this is a newbie question, hope it fits here: I have seen a few times @Kevin Buzzard mentioning a List of theorems, and whether they are formalized in various formal proof systems. The list is names after a person, but i cannot find it anymore. Does anybody know what i am talking about? thanks :)

Mario Krenn (Jun 22 2021 at 13:50):

(deleted)

Alistair Tucker (Jun 22 2021 at 13:51):

https://www.cs.ru.nl/~freek/100/

Anne Baanen (Jun 22 2021 at 13:51):

You might be thinking of Freek Wiedijk's 100 theorem tracker

Mario Krenn (Jun 22 2021 at 13:51):

YES great thanks! :)

Anne Baanen (Jun 22 2021 at 13:52):

(The choice of the 100 theorem is not Freek's, they are just being tracked by Freek)

Cody Roux (Jun 22 2021 at 13:52):

Dang, beat me to it.

Cody Roux (Jun 22 2021 at 13:53):

Surprisingly few remaining on that list, though Kevin contends (probably correctly) that the FLT proof is more work than all the others combined.

Mario Krenn (Jun 22 2021 at 13:54):

Is that page rather updated? Or are there now more than 61/100 proofs formalized in Lean?

Johan Commelin (Jun 22 2021 at 13:55):

https://leanprover-community.github.io/100.html

Anne Baanen (Jun 22 2021 at 13:55):

So we have 62 now

Johan Commelin (Jun 22 2021 at 13:56):

But we usually ping Freek when we have 5 new entries or so

Johan Commelin (Jun 22 2021 at 13:57):

Cody Roux said:

Surprisingly few remaining on that list, though Kevin contends (probably correctly) that the FLT proof is more work than all the others combined.

I think there are only 2 people active on this Zulip that can claim to be experts on FLT. Kevin is one of them, and the other doesn't follow this stream.

Mario Krenn (Jun 22 2021 at 13:57):

OHHH thats quite interesting, thanks Johan! (oh, and congratulations for the success that was mentioned by Peter Scholze/nature few days ago. I was reading the quanta article today again, especially "“It will likely be decades before this is a research tool,” said Heather Macbeth of Fordham University, a fellow Lean user." -- i had to laugh).

Eric Rodriguez (Jun 22 2021 at 14:10):

there's quite a few proofs of these theorems rotting in the queue because they aren't of a fantastic code-style too

Eric Rodriguez (Jun 22 2021 at 14:10):

I'd reckon we're nearing 70 in reality...

Last updated: Dec 20 2023 at 11:08 UTC