Weekly
News about Lean, the theorem prover and programming language.
Edition 2: 6 items published for Jan 8 to Jan 15, 2026.
AxiomProver, an autonomous AI theorem prover built by Axiom, solved 12 out of 12 problems from the Putnam Competition, 8 of them within the strict exam time limit, producing formal proofs in Lean. One combinatorial step in Problem A5 required 2,054 lines of formal proof.
Checked against: LinkedIn post
A Hacker News thread on the claim that Erdos problem #728 "was solved more or less autonomously by AI" drew 619 points and 363 comments. A Harmonic employee said Aristotle, the company's system, can translate an informal English proof into Lean, and commenters debated how to check that a theorem statement is formalized correctly.
Checked against: news.ycombinator.com
A pull request by Sebastian Ullrich bundles all Init module files into a single file with cross-sharing, reducing cumulative size from 325MB to 264MB and openat calls for import Init on Linux from about 2000 to about 80. The pull request is still open.
Checked against: lean4#11965
A merged Lean pull request by Leo de Moura improves the proof term produced by mkFunext, which Sym.simp uses when simplifying lambda expressions. For a 200-lambda benchmark, kernel checking time fell from 148.681 ms to 6.903 ms, and the approach will later come to Meta.simp.
Checked against: lean4#11932
In a LinkedIn post, Martin Ciupa recaps the conversation, in which Terence Tao calls automating formalization (turning ordinary math into proof-assistant-checked form) the near-term change, stresses formal verification over trusting AI blindly, and highlights Lean-style autocomplete that fills a line or two at a time.
Checked against: LinkedIn post
The Lean Together 2026 schedule includes a mix of casual and more formal presentations, with talks running around four hours each day and staggered start times for different time zones. Recordings of all talks are on the Lean community YouTube channel.
Checked against: leanprover-community.github.io