3 stories tagged lean4, newest first.
![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)
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)
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.
463 points by gridentio | 207 comments
Terence Tao's Mastodon post explaining how formalizing his paper in Lean 4 revealed a small bug in an argument for small values of n.