Ship Your Interpreter(basis.ai)
18 points by gopiandcode | 7 comments
Basis blog post describing using LLMs to write a formal semantics for a small language and Lean to prove its interpreter correct down to RISC-V compiled code.
#lean on Hacker News
26 stories tagged lean, newest first.
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.
Lean now ships with verified kernels(leodemoura.github.io)
189 points by matt_d | 68 comments
Leonardo de Moura blog post announcing Lean v4.35.0 ships with lake check, leanchecker, and four additional independent verified kernels for rechecking proofs.
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.
What mathematicians should know about the Lean Theorem Prover: reliability & AI(terrytao.wordpress.com)
178 points by matt_d | 50 comments
Terence Tao blog post on what mathematicians should know about the Lean theorem prover, covering reliability and AI; the capture shows only a browser-check interstitial.
OpenAI Withdraws 3 Math Papers(github.com)
335 points by theemathas | 321 comments
A history.md file in OpenAI's math GitHub repository logging withdrawn and updated math papers, with READMEs explaining gaps and linking retracted manuscripts.
OpenAI withdraws three mathematical results(twitter.com)
355 points by sashank_1509 | 593 comments
Tweet by Dan Roberts announcing updates to OpenAI's GitHub math repo: 6 new Lean formalizations, 19 modifications, and 3 withdrawn results.
Navier–Stokes Lost in Translation(arxiv.org)
321 points by nill0 | 194 comments
arXiv paper arguing that Lean verification of AI-autoformalised proofs, such as a claimed Navier–Stokes blow-up proof, does not guarantee the original natural-language proof is correct.
AI-assisted proof of optimal packing for 11 squares(github.com)
109 points by bluepeter | 52 comments
GitHub repository containing a Lean formalization of the optimality proof for packing 11 unit squares into the smallest square.
Mathematical manuscripts and supporting proof artifacts produced by OpenAI(github.com)
9 points by vikas-sharma | 0 comments
GitHub repository from OpenAI containing mathematical preprints, Lean proof artifacts, and reasoning traces produced by its models.
Anatomy of a Lean proof for software engineers(agostbiro.net)
103 points by abiro | 33 comments
A blog post walking software engineers through the structure of a Lean proof, using a finite automata problem from a theory of computation textbook.
To grieve, or not to grieve?(xenaproject.wordpress.com)
142 points by stabbles | 122 comments
A Xena Project blog post by a mathematician reflecting on whether to grieve as AI advances in formalizing mathematics in Lean, following a post about Anthropic and FLT.
Why Buran Had Four Computers, Not Three(zatona.dev)
9 points by dzatona | 0 comments
Engineering blog post explaining why the Soviet Buran shuttle used four redundant flight computers rather than three, and what a Lean formal proof adds to the reasoning.
A Faster Shortest Path Algorithm(vals.ai)
29 points by leumon | 6 comments
Vals AI blog post describing how ten Claude Opus 5.5 agents found and formally verified in Lean a faster shortest-path algorithm called C-HD.
On the Navier–Stokes Millennium Prize Problem(openai.com)
1295 points by tedsanders | 1045 comments
OpenAI research publication page on the Navier–Stokes Millennium Prize Problem, linking to a paper and a Lean formalized proof.
![Screenshot of cims.nyu.edu: Navier-Stokes – Tristan Buckmaster [pdf]](https://hn.urlbox.com/shots/renders/2026/9/8/63fa481c-8c2c-40ae-af4e-16be796c117e.jpg)
Navier-Stokes – Tristan Buckmaster [pdf](cims.nyu.edu)
1947 points by procedurecall | 798 comments
A PDF statement by mathematician Tristan Buckmaster announcing LLM-assisted, Lean-verified blowup results for Boussinesq, 3D Euler, and porous media equations with smooth forcing.
Formalizing Fermat's Last Theorem(anthropic.com)
743 points by jlebar | 479 comments
Anthropic research post on formalizing the proof of Fermat's Last Theorem, apparently using Claude, with a linked Xena Project blog response.
Human mathematicians are being outcounterexampled(xenaproject.wordpress.com)
456 points by artninja1988 | 225 comments
A Xena Project blog post about mathematicians being outpaced at finding counterexamples, from the blog on mathematicians learning the Lean theorem prover.
Leanstral 1.5: Proof abundance for all(mistral.ai)
353 points by programLyrique | 94 comments
Mistral AI research blog post announcing Leanstral 1.5, a model for generating formal proofs in the Lean theorem prover.
Lean proved this program correct; then I found a bug(kirancodes.me)
375 points by bumbledraven | 167 comments
Blog post describing how fuzzing a formally verified Lean implementation of zlib uncovered a buffer overflow in the Lean runtime.
AI will make formal verification go mainstream(martin.kleppmann.com)
782 points by evankhoury | 394 comments
Martin Kleppmann blog post predicting that AI will bring formal verification with proof assistants like Rocq, Isabelle and Lean into mainstream software engineering.
The Math Is Haunted(overreacted.io)
389 points by danabramov | 182 comments
Dan Abramov's overreacted blog post about writing Lean, a programming language used by mathematicians to formalize theorems and proofs as code.
Milk Kanban(brodzinski.com)
405 points by ladronevincet | 154 comments
Blog post by Pawel Brodzinski describing an office practice of tagging milk cartons with cards to signal restocking, as a simple example of Kanban.
Can AI do maths yet? Thoughts from a mathematician(xenaproject.wordpress.com)
372 points by mathgenius | 317 comments
Blog post on the Xena Project blog by a mathematician discussing whether AI systems can do research-level mathematics yet.
Rosetta 2 creator leaves Apple to work on Lean full-time(linkedin.com)
339 points by ladberg | 102 comments
LinkedIn post by Leonardo de Moura announcing that Cameron Zwarich, creator of Apple's Rosetta 2, is joining the Lean FRO to work on Lean full-time.
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.