Weekly
News about Lean, the theorem prover and programming language.
Edition 27: 13 items published for Aug 27 to Sep 3, 2026.
Palomar, an initiative incubated by the Lean FRO and by ICARM, registers GitHub repository snapshots after checking with the Lean tool Comparator that proofs match the claimed statements, and with a large language model that the informal description matches. Terence Tao stresses that Palomar is not a peer-reviewed journal.
Checked against: terrytao.wordpress.com
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
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
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
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
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
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
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
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
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
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
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
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