Lean formalization of the Hamilton-Perelman proof of the Poincaré conjecture | Hacker News - But Better

Lean formalization of the Hamilton-Perelman proof of the Poincaré conjecture github.com

A general geometry library in LEAN 4. Contribute to qinz1yang/differential-geometry development by creating an account on GitHub.

1 points•nill0•3 days ago•1 comment•

#lean #conjecture #formalization #hamilton #perelman #poincar #proof #lean formalization

1 comment

nill03 days ago

https://x.com/ayushkhaitan343/status/2104289939840176167

Read the full thread on Hacker News →

Related stories

Hamilton–Perelman's proof of Poincaré conjecture is claimed to be autoformalizedgithub.com
Hacker News · 2 points · 2 days ago
AI proof of the Erdős–Sós conjecturearxiv.org
Hacker News · 5 points · 8 days ago
Lean 4 proof of Fermat's Last Theorem: how Claude did it in 11 daysdev.to
DEV Community · 0 points · 3 days ago
Lean Golf – Code golf but you're proving theorems in Leanlean.golf
Hacker News · 1 points · 6 days ago
A Lean Proof Printing Python Union Findphilipzucker.com
Hacker News · 1 points · 5 days ago
A Proof of the Most Informative Boolean Function Conjecturearxiv.org
Hacker News · 3 points · 5 days ago