Weekly
News about Lean, the theorem prover and programming language.
Papers, talks, courses, events, funding, and press. 53 items, newest first.
The AI for Math Fund selected 22 applications representing 30 organizations from more than 470 submissions, bringing its total commitments to $35.1 million. Winners include TorchLean, a Lean-native framework for verified machine learning, and a project turning a Lean 4 visual proofwriting prototype into open-source infrastructure for reading AI-generated proofs.
Checked against: renaissancephilanthropy.org
Markus de Medeiros, Ralf Jung, Lars Birkedal and nine coauthors explore how Lean features like flexible metaprogramming and quotient types can simplify the design and usage of Iris, providing a new implementation of the Iris proof mode with improved performance. Integration with Mathlib supports an application to probabilistic program verification.
Checked against: arXiv:2609.24252
XTX Markets announced $10mn to Lean FRO, a focused research organisation run by Convergent Research, and $10mn to the Mathlib Initiative, each covering core operating costs to 2030. XTX Markets says Lean provided the verification layer in the auto-formalisation of Fermat's Last Theorem.
Checked against: xtxmarkets.com
Greg Brockman says OpenAI pointed Astra at its own systems until it ran out of vulnerabilities to find, putting 25% of its production engineers on defense. Greg Brockman added: "There are ideas, for example, formally verifying all of software, that are possible with AI."
Checked against: @a16z on X
AITP'26, the 11th Conference on Artificial Intelligence and Theorem Proving, takes place from August 30 to September 4, 2026, in the CNRS Paul-Langevin Conference Center in Aussois, Savoy. The program includes a talk by Mario Carneiro on AI-assisted formalization of Pi injectivity and uniqueness of typing for Lean's kernel.
Checked against: aitp-conference.org
Jaume de Dios Pont teaches Computer-Assisted Formalization of Mathematics at New York University, starting Wednesday, September 2, with the Natural Number Game. The schedule runs from Lean basics and Mathlib through program verification and tactic metaprogramming to two weeks on agentic Lean proof generation.
Checked against: nyulean26.github.io
Qianli Ma solves Colombo's 1928 determinant problem, Jef Pauwels proves the Pál and Vértesi conjectures on the I3322 Bell inequality, Zijun Gao and Weihan Zhang falsify an n^(-1/4) near-optimality conjecture from a ChatGPT 5.6 Pro proof attempt, and Gregory Morse shows a multiplicative complexity of exactly nine.
Checked against: arXiv:2608.30221arXiv:2609.00101arXiv:2608.29734arXiv:2608.30238
An essay by Just Different on Proofs and Prompts notes that ChatGPT Pro proved a difficult percolation problem known among colleagues as "p_c < 1" and urges mathematicians not to use their most beautiful conjectures as mere "benchmarks" for the next frontier model.
Checked against: proofsandprompts.com
The paper studies ten results an OpenAI lab published in August 2026 with Lean 4 certificates: kernel-checked proofs total 20.6 MB against 55.6 KB of statements needing human audit (379 to 1), yet those statements contain 218 bespoke definitions. Four weeks later, one result remained disputed over whether its formalization meant what it claimed.
Checked against: arXiv:2608.28997
Leo de Moura's course "Lean 4 for Program Verification in the Age of AI" at the Marktoberdorf Summer School in Herrsching am Ammersee, August 2026, covers dependent type theory, programming and proving in Lean, proof automation and AI, and software verification in Lean.
Checked against: leodemoura.github.io
The workshop runs August 24 – September 4, 2026 at FU Berlin, with group work aimed at formalizing the foundations of polyhedral theory and integrating them into mathlib. Separately, the INdAM Meeting "Lean for the Curious Mathematician" will be held in the historical Palazzone di Cortona in Italy.
Checked against: mathconf.euamosturchet.github.io
On The Peterman Pod, Leo de Moura discusses how formal verification and proof assistants work, Lean's role in recent math results, when software is worth formalizing, and how LLMs plus Lean will change writing software and doing math. The episode is on YouTube, Spotify, and Apple Podcasts, with a transcript.
Checked against: @ryanlpeterman on XLinkedIn post
Tim Sweeney called the response "an exemplary handling of a bug in the Lean theorem prover and proof verifier kernel." The bug was discovered in an AI generated proof, a contributor simplified it down to a straightforward reproduction, and the team fixed it speedily.
Checked against: @TimSweeneyEpic on X
In a LinkedIn post, Alexander Gerko says that over the last month he "vibe researched" several PhDs' worth of maths results in his former field, complete with Lean formalization, including a claimed counterexample to a top-5 major conjecture. Gerko predicts "50 years' worth of maths progress in the next 2 years."
Checked against: lnkd.in
Amazon is providing substantial, long-term financial support to the Lean Focused Research Organization (FRO), the team building Lean, which Amazon calls the single largest donation in the FRO's history. Amazon ties the investment to agentic safety and cites Lean-based verification in Policy in Amazon Bedrock AgentCore, SampCert, and AWS Neuron.
Checked against: amazon.scienceitpro.com
Leo de Moura presented "The Lean Theorem Prover: Design, Evolution, and Impact" at FLoC 2026 in Lisbon on July 26, 2026. Kim Morrison and Leo de Moura followed with a talk at IJCAR (Monday July 27 at 11:50 am) on grind, a new extensible tactic based on SMT techniques.
Checked against: leodemoura.github.io
Son Ho's talk at the meetup, hosted by UTUM Venture Labs, previewed Formal Spec driven Development: AI implements a spec and generates its constraints using autoformalisation, while humans write the spec and check that the constraints cover it. Lean FRO's Munich-based team, including Head of Engineering Sebastian Ullrich, attended.
Checked against: LinkedIn post
Gwern Net's research proposal would measure coding LLM perplexity over growing codebase context to estimate scaling laws of predictability by language. The essay predicts Lean suffers from a very high constant but would have the best scaling exponent, and so would eventually cross over more popular languages such as Python.
Checked against: gwern.net
In a post on X, Dwarkesh Patel described Grant's speculation that AIs could fork Mathlib, the Lean library of formalized math concepts and proofs, and build a "parallel math civilization." Dwarkesh Patel wrote that Lean guarantees any new conjectures would be logically valid, and that whether they would be interesting is another matter.
Checked against: @dwarkesh_sp on X
In a June 2026 talk, Leo de Moura (Senior Principal Applied Scientist, AWS, and Chief Architect, Lean FRO) described AWS projects built with Lean, including Cedar, a verified authorization policy language, SampCert, verified differential privacy, and Waimea, a tensor compiler for Trainium. The slides are written in Verso.
Checked against: leodemoura.github.io
Software Foundations, a series of textbooks on formal proof and foundations of programming languages formalized in Rocq, is being translated to Lean for Fall courses at Penn and elsewhere. Benjamin Pierce says the team is ready to add a few people, especially educators, and will need alpha-testers later in the summer.
Checked against: leanprover.zulipchat.com
Quanta Books published The Proof in the Code on June 9, 2026, in which Kevin Hartnett tells the story of the birth and rise of Lean, from a bug-checking program at Microsoft Research developed by Leo de Moura to its adoption by mathematicians and tech firms.
Checked against: amazon.com
Leo de Moura, Chief Architect of the Lean FRO, spoke on May 12, 2026 at the Science x AI Summit in Palo Alto (May 12-13, in person and online). The slides, written in Verso, cover Mathlib, IMO-level AI provers using Lean, and verification work on Cedar and SymCrypt.
Checked against: leodemoura.github.iosair.foundation
Leo de Moura, Chief Architect of the Lean FRO, gave the talk "Lean: Machine-Checked Mathematics and AI Collaboration" at the University of Washington on May 8, 2026. The slides open with a general-purpose AI that converted zlib (a C compression library) to Lean, passed the test suite, and proved the code correct.
Checked against: leodemoura.github.io