r/math • u/al3arabcoreleone • 4d ago

What mathematicians should know about the Lean Theorem Prover

https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/

A brief explanation of proof assistants

365 Upvotes

97% Upvoted

33 comments sorted by

View all comments

56

u/togstation 4d ago

guest post by Thomas Hales on Terence Tao's blog.

IMHO this is worth a look.

23

u/LuckyLuke123809 3d ago

I really enjoyed reading it. Probably old stuff, but this reference to Gödel's second incompleteness theorem is really sharp; Lean cannot certify itself.

This relative consistency proof for Con-Leche is kind of a big deal, but the closing words are correct: we need to do better.

8

u/Keikira Model Theory 3d ago

Isn't the whole point of Gödel's incompleteness theorems that we can't do better in principle?

5

u/Fit_Desk_2643 3d ago

Gödel's incompleteness says that we can't do best, We can always do better. We have the same issue for ZFC, but we have a much deeper understanding of ZFC than of Lean's type theory

0

u/happyapy 3d ago

I don't think so. We can likely do better, we just can't say we've perfected it.