Weekly

News about Lean, the theorem prover and programming language.

Lean Weekly: the latest news

AI and formalization

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.orgIsaacRudich/SubexponentialDeterministicFactoring

Verification

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

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

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

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/zenosleanprover.zulipchat.comzenos v0.1.0-preview

Verification

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.

The case study title “Tensordyne’s most complex block and early exploration for its next chip” in white over a picture in the Harmonic blue, with the Harmonic logo
Image: harmonic.fun

Checked against: harmonic.fun

Verification

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.

The case study title “Speed up your code without wondering what you broke” in white over a picture in the Harmonic blue, with the Harmonic logo
Image: harmonic.fun

Checked against: harmonic.fun

Verification

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/RatpointsLeanleanprover.zulipchat.comMichaelStollBayreuth/ratpoints

AI and formalization

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.

The CFSG blueprint as a corpus wheel, with the classification theorem at the centre.
Image: axiommath.ai

Checked against: axiommath.aicfsg.axiommath.aiAxiomMath/CFSGhexagonmath.org

Verification

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.

Image: aqueduct.verina.io

Checked against: aqueduct.verina.ioarXiv:2610.30188@0xlf_ on X

Lean core

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

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.

Image: x.com/leanprover

Checked against: @leanprover on Xfunctional.cafebsky.app

Verification

Natalie Marleny announces formal-git, modelling about 30% of Git in Lean 4

Built over two months with heavy use of coding agents, the project proved more than 8,000 theorems of varying usefulness and uncovered more than 100 potential defects in Git v2.55, including at least two possible security vulnerabilities. Its differential random testing harness and more than 10,000 unique tests will be open-sourced after responsible disclosure.

Image: x.com/NatalieMarleny

Checked against: @NatalieMarleny on X

Verification

John Zhuoyang Ye and Jens Palsberg verify fault-tolerant quantum compilation in Lean

The paper introduces QPPM, a language for Pauli-product measurement programs, and verifies lowering of Clifford+T circuits to QPPM and an optimizer that eliminates measurements, fuses and reorders rotations, and schedules logical rounds. On QASMBench, verified fusion and scheduling reduce logical measurement depth by a median of 17.9%.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2610.31694paperswithlean.com

AI and formalization

Resolution uses Claude Fable 5.1 to formalize Hironaka's resolution of singularities

The library, written in Lean 4 over Mathlib, proves Hironaka's main theorems in characteristic zero and their refinements by Kollár, Włodarczyk and Bierstone–Milman, for algebraic schemes and analytic manifolds and spaces. Chris Elliott at Resolution directed and audited the automated formalization process, and the code is licensed under Apache License 2.0.

Checked against: resolutionorg/hironakaresolutionorg.github.ioreservoir.lean-lang.org

Verification

Miles Cranmer's AI agents model Julia code in Lean and find bugs

Lean definitions mirror Julia functions line by line, and each property ends proven, or refuted with a concrete counterexample and a pure-Julia reproducer. In Julia Base and several standard libraries, 400 of 910 properties were refuted and 75 issues filed on JuliaLang/julia; DynamicExpressions.jl, the expression-tree package behind PySR, merged 38 Lean-derived fixes.

Checked against: MilesCranmer/julia-in-lean

Verification

Thomas Coratger announces EthLib, a Lean 4 library for Ethereum

The library, hosted at github.com/ethereum/EthLib, launched with the goal of bringing Ethereum's primitives, specifications and theorems into one place, building a shared foundation for formally specifying and proving things about Ethereum.

Checked against: @tcoratger on X

Verification

Katzenpost's Lean library Cryptlib implements the Sphinx cryptographic packet format

Cryptlib's Sphinx packets are binary compatible with the Katzenpost mix network's Go implementation, including with a post-quantum/classical hybrid key encapsulation method (X25519 and ML-KEM-768) per hop. The AGPLv3-licensed library is for modeling protocols and proving their properties; each kind of primitive has a Lean structure with proposition fields that every instance must satisfy.

Checked against: katzenpost/cryptlibcryptlib.ioreservoir.lean-lang.org

Lean core

Joachim Breitner releases con-agua, a Lean checker with verified x86 assembly

Written by AI under Joachim Breitner's supervision, con-agua is an x86 assembly port of the external Lean checker con-leche and requires the Kraken x86 semantics to be correct in place of the Lean compiler and runtime. A 5MB assembly file and a 200-line main.c, plus one data file, are all it needs.

Checked against: leanprover/con-agualeanprover.zulipchat.com

Verification

AssureCode uses Lean for structured justification of AI-generated code

Logan Murphy and coauthors describe AssureCode, which autoformalizes developer intent into Lean specifications for human approval, then decomposes claims via Lean templates, with Lean checking an agent's decomposition-soundness proofs. On HumanEval, LiveCodeBench and MBPP samples with four LLMs, a single run recovered most of an iterative LLM baseline's concerns and surfaced additional ones.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2610.29758paperswithlean.com

AI and formalization

Wolfram Institute publishes reference Lean environment for Rule 30 Prize submissions

The verifier checks every submission against exactly this Lake project (Lean 4.35.0, Mathlib's v4.35.0 tag), and the submissions site has instructions for AI agents. The kit contains the official statements of Problems 1 and 2, proved partial results, 163 equivalences and 49 sufficient conditions for Problem 1, and 14 equivalent forms of Problem 2.

Checked against: WolframInstitute/Rule30PrizeKit

Verification

Anand Kumar Keshavan announces lean-qverify for verifying quantum circuits in Lean 4

The open-source project includes a Lean library, a Qiskit integration, and a free workbook with executable examples covering circuit specifications, semantic proofs, Quantum Hoare Logic and ZX-calculus. Anand Kumar Keshavan calls the current implementation an initial research and educational framework, welcomes independent technical reviews, and is interested in collaborating on compositional proof techniques.

Checked against: akkeshavan/lean-qverifyleanprover.zulipchat.comakkeshavan.github.io

AI and formalization

Pranava Kumar registers a Lean proof of Nivat's conjecture with Palomar

The entry formalizes Pranava Kumar's manuscript, proving that any configuration on the integer plane over a finite alphabet with at most k times n distinct k by n patterns has a nonzero global period. Its independent Challenge states the full conjecture using only standard Mathlib notions; the 339-file proof needs only Lean's foundational axioms.

Checked against: palomar-registry.orgPranavaKCode/nivat-lean

More news