42 stories tagged formal-verification, newest first.
429 points by johnbender | 265 comments
Anthropic research post describing how Claude produced formal proofs of crash-freedom for RISC-V binaries of 123 OSS-Fuzz open-source libraries, finding bugs along the way.
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.
112 points by laginimaineb | 49 comments
Landing page for Maxwell by doubleAI, a 'Code Execution Model' that optimizes running code for hardware and data with formally proven equivalence, offering early access.
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.
8 points by stmonty | 3 comments
An HTML tutorial by John Harrison and Juneyoung Lee giving a quick-start, example-driven guide to using the HOL Light theorem prover.
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 teorth.github.io: Terence Tao: Math 2.0 [pdf]](https://hn.urlbox.com/shots/renders/2026/10/11/5fa8cc24-3e1c-4321-8c9a-8aee16c4af72.jpg)
533 points by Anon84 | 530 comments
PDF slide deck titled "Math 2.0" by mathematician Terence Tao, dated October 2026, apparently from a Caltech talk.
47 points by o8vm | 35 comments
GitHub repository for hibana, a Rust library providing choreography-derived runtime enforcement for distributed protocols.
![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.
127 points by peter_d_sherman | 37 comments
LWN article describing Eurydice, a project that compiles Rust code into readable C for use with verification tools and platforms lacking a Rust compiler.
50 points by danielmorozoff | 5 comments
New Scientist article reporting that OpenAI's human-readable Navier-Stokes proof and its computer-formalized version do not match due to mistranslation into code.
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.
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.
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.
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.
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.
35 points by nvtop | 38 comments
An essay by Christian Szegedy published as a Google Doc, reflecting on the future of mathematics, opening with his background in Hungarian math education.
![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.
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.
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.
223 points by b-man | 47 comments
Hillel Wayne's Computer Things newsletter post on the limits of what TLA+ can verify, pushing back on claims that TLA+ with AI models will make AI-written code reliable.
97 points by matt_d | 48 comments
A Reasonable blog post introducing TLA+ and discussing how temporal specifications, proof systems, and AI agents can combine to produce specified, verified software.
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.
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.
564 points by nicolas-siplis | 287 comments
Landing page for Bend, a fast programming language with Python-like syntax, CUDA parallelism, and Lean-style proofs to verify AI-written code.
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.
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.
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.
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.
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.
730 points by Poudlardo | 178 comments
Mistral AI announcement of Leanstral, an open-source code agent for Lean 4 aimed at trustworthy coding and formal proof engineering.
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.
358 points by vitalnodo | 121 comments
Homepage of Ironclad, a formally verified, real-time capable, Unix-like OS kernel written in SPARK and Ada with POSIX compatibility and MAC.
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.
359 points by meetpateltech | 74 comments
GitHub repository for DeepSeek-Prover-V2, DeepSeek's model for formal theorem proving, containing a paper PDF, README, model license, and miniF2F solutions.
447 points by todsacerdoti | 142 comments
Blog post by Jonathan Protzenko describing how CPython now uses the formally verified HACL* library for all its default hash and HMAC algorithms.
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.
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.
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.
323 points by todsacerdoti | 119 comments
A Dreamwidth blog post by Graydon Hoare with notes on Rust, mutable aliasing, and formal verification; the capture shows only a captcha check page.
327 points by p4bl0 | 103 comments
Formal Land blog post describing a best-effort translation of Rust's core and alloc crates into Coq using their coq-of-rust tool for formal verification.
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.