Lean Weekly: the latest news

∃

AI and formalization·Oct 29

Lean becomes first to formalize all 100 theorems on Freek Wiedijk's list

Freek Wiedijk's page tracking formalizations of 100 theorems, last modified October 29, 2026, shows Lean at 100, with HOL Light and Isabelle next at 95. Kim Morrison reports that the 100th theorem completed in Lean, a strong formulation of Green's theorem (TauCeti.Green.green_ac_index_one), landed in Tau Ceti, a library of AI-authored Lean mathematics.

⊢Checked against: kim-em.github.io·cs.ru.nl·taucetiproject.org·leanprover.zulipchat.com

⊨

Verification·Oct 29

Mathstodon user markusde posts about porting xv6 to Iris-Lean

The post includes one attached image and thanks @ahuoguo for noticing the update.

⊢Checked against: mathstodon.xyz

∃

AI and formalization·Oct 29

Juan J. Manfredi completes Lean formalization of OpenAI's infinity-harmonic estimates

The formalization, built on Mathlib, proves the main results of OpenAI's 4 October 2026 preprint, including that infinity-harmonic functions (viscosity solutions of the infinity-Laplace equation) on connected open sets in dimensions 3 and higher are C¹, using only Lean's three standard axioms. Claude agents wrote the Lean proofs with Trellis, an AI-assisted formalization pipeline.

⊢Checked against: palomar-registry.org·na0b/infharmonic-lean

∃

AI and formalization·Oct 29

Anthropic publishes Lean formalization of Claude's refutation of the Exponential Time Hypothesis

Anthropic's eth/ project, a machine-checked Lean 4 formalization, states that a single deterministic Turing machine counts the satisfying assignments of every k-CNF with at least two clauses on at least four variables, each of which occurs, within a step bound that refutes the hypothesis. Claude's paper is in the project folder.

⊢Checked against: anthropics/formal-math

¶

Papers and events·Oct 27

XTX Markets gives £5 million to Imperial College London for Langlands Lab

The lab for AI-assisted mathematics, led by Kevin Buzzard, will focus on the Langlands program, which seeks connections between fields, particularly number theory and analysis. It aims to produce new results verified in Lean and begins operating in 2027, with the grant supporting five PhD students and three postdoctoral researchers over four years.

⊢Checked against: imperial.ac.uk

λ

Lean core·Oct 23

Leo de Moura speeds up kernel checking of lia and grind proofs

Lean's lia (cutsat) now shares proofs across grind case splits, for up to 2.8x faster elaboration and up to 200x faster kernel checking on goals with many case splits. Kernel-friendly certificates for lia, grind's ring solver, simp +arith and grind linarith followed; the ring certificates cut kernel instructions by 51.5% across 40 benchmark files.

⊢Checked against: lean4#15905·lean4#15911·lean4#15943·lean4#15981·lean4#15983

λ

Lean core·Oct 20

Sebastian Graf merged vcgen +jp, which verifies code after a split once

Without +jp, vcgen copies the code after an if or a match into every branch, so the number of copies doubles with each consecutive split. With +jp, VC generation grows linearly with the number of splits, and the shared code is verified under a hypothesis stating what each branch knows at its end.

⊢Checked against: lean4#14398

¶

Papers and events·Oct 29

Benjamin Pierce announces Agentic Proof Engineering, a Spring 2027 course at Penn

The semester course is on building formal proofs about software systems at scale, in collaboration with AI agents, and will also be delivered as a live webinar for participants outside Penn. Some lectures and projects will be phrased in terms of Lean, though fluency with the specifics of Lean will not be needed.

⊢Checked against: cis.upenn.edu

λ

Lean core·Oct 24

Leo de Moura makes grind failure messages short by default

Pull request #15906 made diagnostics opt-in via +verbose, so failures showed only the remaining goal and a hint; collecting and printing diagnostics took about 38% of the time spent on easy failing lia goals. Pull request #16073 shortened the failure message further, naming the invoked tactic, such as lia, without printing the goal.

⊢Checked against: lean4#15906·lean4#16073

λ

Lean core·Oct 20

Mac Malone opens Lake pull request to reduce build-store contention

The pending change (#15805) has Lake first fetch transitive artifacts from a single build-store snapshot, falling back to the real build store only when an artifact is missing. Mac Malone also opened #16083 to benchmark Lake's module setup computation, which experiments show is a significant scalability chokepoint in projects with thousands of modules.

⊢Checked against: lean4#15805·lean4#16083

¶

Papers and events·Oct 29

GenProof paper on verifying Minecraft redstone circuits uses Lean's bv_decide

Mike Murunov and Maksim Borisov's gate accepts a redstone layout only with a machine-checkable certificate of equivalence to its Verilog specification. Lean 4 re-proves the claim, unfolding it to one 4-bit equation per node and calling bv_decide, which bit-blasts, runs the CaDiCaL solver and checks its proof with a verified checker.

⊢Checked against: paper (pdf)

∃

AI and formalization·Oct 29

Troy Lee formalizes László Babai's graph isomorphism algorithm using an AI agent

With László Pyber's analysis replacing the classification of finite simple groups, the formalization proves that a single-tape Turing machine (Mathlib's Turing.TM0) decides whether two simple graphs are isomorphic within a quasipolynomial number of transitions. The agent (Claude Code, with Claude Opus 5.5) wrote the Lean code from 18 to 29 October 2026.

⊢Checked against: palomar-registry.org·troyjlee/graph-iso-lean

⊨

Verification·Oct 28

Adam Gall publishes lean-sudo, a drop-in sudo replacement written in Lean 4

Its policy, environment and authentication logic is formally verified, with 498 hand-written theorems. On Ubuntu, lean-sudo reads the existing /etc/sudoers, /etc/sudoers.d and /etc/sudo.conf, uses the system's PAM stack, and passes the same 1113-test end-to-end suite as the original sudo, a large C program written around 1980 with a decades-long history of security bugs.

⊢Checked against: adamgall/lean-sudo

⊨

Verification·Oct 28

holmesworcester publishes Lean Quiet, a chat app written mostly in Lean

The iOS and Android app uses Lean for everything from TCP packets to pixels; 429 of its 586 theorems are about the code that runs. Because it is local-first, end-to-end encrypted, and peer-to-peer, many properties that would normally depend on a server operator are provable over all possible deployments, assuming user device integrity.

⊢Checked against: holmesworcester/lean-quiet

∃

AI and formalization·Oct 28

Scott Armstrong and Zohar Komargodski formalize the positive-measure KAM theorem in Lean

The headline theorem is proved: for a nearly-integrable Hamiltonian with a small enough perturbation, most of phase space is filled by invariant tori carrying quasi-periodic motion. Agents prove the frozen statements (approved line by line, never edited); 11 of 22 are proved so far, with 73,724 of an estimated 117,000 lines of Lean.

⊢Checked against: scottnarmstrong/KAM-dev

⊨

Verification·Oct 28

Open-source desktop OS ZENOS releases first preview with Lean-proved security decisions

ZENOS's services ask zenos-decide, built from the same Lean definitions as the proofs, whether a file opens, content may reach a printer or AI, and a send is allowed, treating missing or unreadable answers as refusals. The theorems rest only on Lean's standard axioms, but the unaudited preview is not for real sensitive data.

⊢Checked against: zenos-org/zenos·leanprover.zulipchat.com·zenos v0.1.0-preview

∃

AI and formalization·Oct 28

Anthropic's Claude generates Lean proof of subexponential deterministic factoring

Isaac Rudich and Louis-Martin Rousseau registered the proof that one deterministic Turing machine computes the smallest prime factor of every natural number N in time N^{o(1)}; the best previously published deterministic bounds known to the authors have exponent 1/5. The authors audited the statement and did not read the proof, which Lean checks.

⊢Checked against: palomar-registry.org·IsaacRudich/SubexponentialDeterministicFactoring

⊨

Verification·Oct 27

Harmonic's Aristotle proved 185 properties of Tensordyne's most complex block

Aristotle, an AI that formally verifies software and hardware, also refuted 56 properties of the 12.2 million gate-equivalent block, each with a reproducible counterexample, exposing bugs up to 110,000 cycles after reset. Counting earlier Aristotle runs on sub-blocks, Tensordyne found 8 bugs early in its next chip's design cycle.

⊢Checked against: harmonic.fun

⊨

Verification·Oct 27

Harmonic's Aristotle fixes three LibTomMath bugs and verifies optimized routines

Aristotle, Harmonic's AI that formally verifies software, found and repaired three bugs in LibTomMath 1.2.0, which supplies large-integer arithmetic to Tcl and Dropbear SSH. Aristotle then optimized two arithmetic routines, making modular exponentiation 31–38% faster in benchmarks, and proved them against the repaired code's specifications for results, memory safety, errors, and stored values.

⊢Checked against: harmonic.fun

⊨

Verification·Oct 27

Michael Stoll had Claude build a verified Lean 4 model of ratpoints

Claude mirrored ratpoints, Michael Stoll's C program that finds rational points on hyperelliptic curves, in Lean function by function and proved, as Comparator certified, that the model meets a short specification. Michael Stoll called the work token-intensive enough to use up a Max 20x subscription's weekly Opus 5.5 allowance within three to four days.

⊢Checked against: MichaelStollBayreuth/RatpointsLean·leanprover.zulipchat.com·MichaelStollBayreuth/ratpoints

∃

AI and formalization·Oct 26

Axiom Math formalizes the classification of finite simple groups in Lean

The complete formalization follows the first-generation proof (thousands of journal pages by about a hundred mathematicians), and Lean's kernel checks every logical step. Axiom Math engineers and mathematicians directed AI agents over 24 days, producing approximately 43.1 million lines of code and finding an issue in a published argument for the Unbalanced Group Theorem.

⊢Checked against: axiommath.ai·cfsg.axiommath.ai·AxiomMath/CFSG·hexagonmath.org

⊨

Verification·Oct 20

Zhe Ye and coauthors propose agentic verified optimization in Lean 4

Agents return faster code plus a Lean proof that it equals the original, which serves as the specification. The agents did so for 156 of 189 Verina functions, and 92 proved rewrites sped up 47 of 51 scenarios in 17 applications the authors' Aqueduct framework migrated to Lean from C, C++, Go, or Rust.

⊢Checked against: aqueduct.verina.io·arXiv:2610.30188·@0xlf_ on X

λ

Lean core·Oct 26

cedar-policy publishes lean-parser-generator, which generates validated LR(1) parsers in Lean

The tool turns an LR(1) grammar in a .lig file into a compiled Lean parser, plus certificates that Lean checks to prove the parser agrees with a generated dependent specification. It follows the a-posteriori validation architecture also used by Menhir's verified back end, so the automaton construction and code generator need not be trusted.

⊢Checked against: cedar-policy/lean-parser-generator

¶

Papers and events·Oct 26

Software Verification in Lean comes to Stanford University on November 7

Co-organized by the Beneficial AI Foundation and the Lean FRO, the day of public lectures covers Rust verification with the Aeneas framework, low-level software verification, and formally verified OS kernels. Speakers include Max Tegmark, Shaowei Lin, Leo de Moura, Jonathan Protzenko, Andres Erbsen, and Mike Dodds; a livestream will be available, with recordings afterward.

⊢Checked against: @leanprover on X·functional.cafe·bsky.app