Weekly
News about Lean, the theorem prover and programming language.
Julia Markus Himmel merged a change that compiles mimalloc as part of the Lean runtime, and Sebastian Ullrich moved rarely-updated Core.Context fields into a cold subobject (mathlib4: -0.82% instructions, -2.03% wall-clock). Lean also updated to mimalloc 3.4.5, fixing a Windows memory leak, and CI changes should halve merge queue run times.
Checked against: lean4#15017lean4#14982lean4#15060lean4#15123
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
A meta issue by Arthur Adjedj, worked out with @nomeata, plans kernel changes that move feature selection for inductives to the elaborator and aim for a decidable, transitive definitional equality algorithm. Recursive predicates like Acc would lose large elimination, and the kernel changes would ideally ship in a single release.
Checked against: lean4#14977
Arthur Adjedj's plan aims for a kernel that is easier to implement bug-free and to verify, with a decidable, transitive definitional equality algorithm and inductive features declared explicitly by the elaborator. Recursive predicates like Acc would lose large elimination, and kernel changes would ship in a single release.
Checked against: lean4#14977
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
Yinjie Li presents an independently obtained, structurally different proof of the strict even-dimensional case of the Harwit and Sloane conjecture, formalized in Lean 4 conditional on Frankel and Urschel's Lemma 2.1 as an explicit external input. Finite evaluations use Lean's native evaluator, with their trust boundary documented.
Checked against: arXiv:2608.29750
Alex Meiburg's eink0rn, a clean-room Lean 4 kernel in Haskell generated mostly by Claude, was merged into the Lean Kernel Arena, which tests and benchmarks proof checkers for Lean. In the current round it answers all 72 invalid and 136 valid tests correctly and checks the mathlib test in 28.4 minutes.
Checked against: lean-kernel-arena#177arena.lean-lang.org
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
Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen and Tianyi Peng introduce Prove2Me, where users launch formalization "missions" and AI agents contribute Lean proofs toward completion, building on and reusing one another's results. One listed mission targets Mathlib's open conway_99 problem on a strongly regular graph with parameters (99,14,1,2).
Checked against: arXiv:2608.28433prove2.me
Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková and Christoph Thiele released a blueprint and Lean 4 formalization of a quantitative strengthening of Tao's norm-convergence theorem, answering an open question of Avigad and Rute. The proof was autoformalized during a one-week period using coding agents under human supervision, producing roughly 107k lines of code.
Checked against: roos-j/lean-nctarXiv:2608.27321
The roadmap covers lake check commands for external kernel checking, a code formatter, Nerodia (a Lean/Python FFI inspired by PyO3), and faster typeclass inference. It also covers the FRO's AI projects Tau Ceti, Hex, and Palomar, and defers investment in debugger infrastructure.
Checked against: lean-lang.org
The Vilin97/MazurTheorem repository targets the classification of rational torsion on elliptic curves, using Mazur's degree-one formal-immersion argument at the auxiliary prime 5. The project reports an integrated score of 17.2% on its 48-node, 1,000-point theorem DAG, and it accepts claims only on contracts marked open or research_open.
Checked against: Vilin97/MazurTheorem
The repository adds passwordless sign-in, SQL migrations, OpenTelemetry traces and logs, an MCP endpoint, and deployment to AWS Lambda, built on Paul Butcher's own Lean libraries. Markup is typed and formally verified (a <div> inside a <p> is a type error), and lean-json is proved correct against the grammar of RFC 8259.
Checked against: paulbutcher/lean-todomvc-max
Sebastian Ullrich merged leanchecker-paranoid, a variant of leanchecker built with allocator hardening, and lake challenge, a frontend to comparator that simplifies its setup. Joachim Breitner's lean-inductive-models performs translation validation of user-defined Lean inductives into an extensional type system with a small hard-coded inductive basis.
Checked against: lean4#14885lean4#14884nomeata/lean-inductive-modelsarena.lean-lang.org
The CSLib Initiative, a program of Renaissance Philanthropy, supports the growth of the CSLib open-source project (a focused effort on formalizing computer science in Lean) in the same way that the Mathlib Initiative supports Mathlib. Its site lists a team, a Strategic Advisory Board, and a roadmap of operational goals guiding its funding.
Checked against: cslib.io
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
Jiaxin Yuan and coauthors introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics, finding formalization remains a major bottleneck. Separately, Wenqian Ye and coauthors present ProofEvolve, where the Lean kernel verifies every proof transition. It achieves the highest average solve rate among the evaluated proof systems on three competition-level Lean benchmarks.
Checked against: arXiv:2608.25449arXiv:2608.26334
The competition asks participants to improve the performance of verified computation in the Lean 4 kernel (the trusted component that checks every proof accepted by Lean) with optimized implementations and machine-checked proofs of correctness. Stage 1 pre-registration is open, with the official launch on September 15, 2026.
Checked against: @Leonard41111588 on XLinkedIn post
Wojciech Różowski merged a Lean pull request that generates strong_coinduct for coinductive_fixpoint predicates, strengthening coinduct, plus strong_induct for inductive_fixpoint ones. A second merged pull request adds a monotonicity_by clause so users can prove monotonicity of the underlying fixpoint functor with an explicit tactic block when automatic proof search fails.
Checked against: lean4#14855lean4#14861
Daniel Selsam used OpenAI internal models to find soundness issues in the official Lean kernel and runtime from July 30 to August 20, and Lean v4.33.1, released August 21, fixes all of them. Starting with Lean v4.35.0, lake check will export and recheck projects using lean4checker.
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
Scott Armstrong wrote on X that in March, Lean formalization was not possible for his papers, and by August it had become essential and increased the efficiency of his workflow dramatically. Scott Armstrong says the papers are getting written informally and finished much faster because of the Lean formalization.
Checked against: @scottnarmstrong on X