20 stories tagged theorem-proving, newest first.
111 points by smilelamp | 148 comments
Guest post by Francesco Maggi on Terence Tao's blog discussing whether AI and large language models will bring a golden or dark age for mathematics and science.
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.
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.
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.
15 points by philipfweiss | 1 comments
Scott Aaronson's Shtetl-Optimized blog post reacting to OpenAI releasing hundreds of AI-solved major math results, including one his wife worked on.
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.
9 points by vikas-sharma | 0 comments
GitHub repository from OpenAI containing mathematical preprints, Lean proof artifacts, and reasoning traces produced by its models.
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.
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.
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.
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.
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.
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.
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.
1300 points by ocfnash | 496 comments
Google DeepMind blog post announcing AlphaProof and AlphaGeometry 2 reaching silver-medal standard on International Mathematical Olympiad problems.
516 points by FlawedReformer | 158 comments
Google DeepMind research blog post introducing AlphaGeometry, an AI system that solves olympiad-level geometry problems.
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.