How to Formalize All of Mathematics(xenaproject.wordpress.com)
62 points by practal | 53 comments
A Xena Project blog post by Kevin Buzzard's group on how to formalize all of mathematics using the Lean theorem prover.
#mathlib on Hacker News
5 stories tagged mathlib, newest first.
Vi Hart's Big Navier-Stokes Post(patreon.com)
15 points by signa11 | 3 comments
A Patreon post by Vi Hart, in six parts, about the Navier-Stokes problem, the Lean theorem prover and Mathlib, OpenAI, and the politics of mathematics.
![Screenshot of jdb19937.github.io: The logarithms of rational numbers have irrationality exponent 2 [pdf]](https://hn.urlbox.com/shots/renders/2026/10/10/3771ae7f-7658-4460-b339-470c583bc18c.jpg)
The logarithms of rational numbers have irrationality exponent 2 [pdf](jdb19937.github.io)
16 points by jdb1729 | 3 comments
A math paper by Dan Brown claiming the irrationality measure of log of any rational number other than 1 is 2, with the proof formalized in Lean 4 over Mathlib.
![Screenshot of jdb19937.github.io: The reciprocal sum of the prime-prefix-free numbers converges [pdf]](https://hn.urlbox.com/shots/renders/2026/10/9/782dd723-5a0f-4ad2-9aa4-d11ae9b968a4.jpg)
The reciprocal sum of the prime-prefix-free numbers converges [pdf](jdb19937.github.io)
15 points by jdb1729 | 14 comments
A math paper proving, assuming the Riemann Hypothesis, that the reciprocal sum of prime-prefix-free integers (OEIS A287117) converges, with bounds verified in Lean 4.
Fermat's Last Theorem – how it’s going(xenaproject.wordpress.com)
422 points by verbify | 206 comments
Kevin Buzzard's Xena Project blog post giving a progress update on formalizing the proof of Fermat's Last Theorem in the Lean theorem prover.