Weekly

News about Lean, the theorem prover and programming language.

Lean Weekly: the latest news

AI and formalization

Polona Durcik registers AI-generated Lean proof on triangles in positive-density sets

The Palomar registry entry formalizes the theorem that every Lebesgue measurable planar set with positive upper Banach density contains a translated and rotated copy of every sufficiently large dilate of any fixed noncollinear triangle. The proof was developed using GPT 6 Astra Pro with human oversight; Claude Opus 5.5 Medium generated the Lean formalization.

Checked against: palomar-registry.orgdurcikp/lean-trianglesinplane

AI and formalization

Alpha Squared Labs formalizes the Atiyah–Singer index theorem in Lean 4

The project also covers the theorem's cohomological and twisted spin Dirac formulations, and Comparator, a harness checking seven independently written propositions, reported acceptance by both Lean's default kernel and the Nanoda kernel. AI assisted with Lean statements and proof development under human maintainers' responsibility; no new mathematical theorem is claimed.

Checked against: alpha-squared-labs/Lean-Atiyah-Singer

AI and formalization

Zayn Blore machine-checks the Dixmier conjecture's failure in dimension 3 and above

The Palomar registry entry proves in Lean that, over any field of characteristic zero and in each dimension, the Dixmier conjecture implies the Jacobian conjecture, and checks an explicit counterexample to the Jacobian conjecture in every dimension of 3 or more. Its four statements are copied verbatim from Google DeepMind's Formal Conjectures.

Checked against: palomar-registry.orgzblore/fc-dixmier-jacobian

Verification

Anthropic releases FlashProve, with Lean proofs of its security properties

Anthropic released FlashProve, which uses a zkSNARK (a type of cryptographic proof) to prove which AI model answered a request. Anthropic used Lean to specify FlashProve's protocol and prove completeness (honest proofs are accepted), soundness (fake proofs are rejected) and zero-knowledge (proofs hide the model's weights), and shipped an executable, provably correct Lean verifier.

Anthropic logo
Image: anthropic.com

Checked against: anthropic.comanthropics/FlashProve

Verification

Kiro proves properties of its own agent harness in Lean

Kiro wrote Lean models of 26 functions from its TypeScript, Rust, and Python harness (the code managing context, permissions, and state), proving 70 of 96 properties; 18 falsified ones reproduced on the real code. “Lean’s kernel checks every proof, the real code checks every finding,” says the post, which Swami Sivasubramanian shared on LinkedIn.

Kiro proves properties of its own harness in Lean - Blog post by Yaroslav Kharkov, Ferhat Erata, Behrooz Omidvar-Tehrani, Rajdeep Mukherjee
Image: kiro.dev

Checked against: kiro.devLinkedIn post

AI and formalization

Thanin Quartz and coauthors prove 2×2 matrix mortality undecidable, checked in Lean

Matrix mortality asks whether some product of matrices from a finite family equals the zero matrix; only dimension two was open, with higher dimensions known undecidable since 1970. The result holds for families of 5,799 distinct 2×2 integer matrices, and a Lean 4 formalization checks the full reduction from halting, without project-specific axioms.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2611.06562paperswithlean.com

Verification

Jesse Comer and coauthors present Whiel for Lean-certified relational program verification

Whiel verifies programs whose states are database instances against Hoare specifications: an LLM proposes loop invariants, and the Vampire first-order theorem prover checks their verification conditions. An independent certifier constructs Lean proofs of the original specification or its negation; the 86 benchmark tasks have certified reference answers, 69 valid and 17 invalid.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2611.05612JesseComer/whiel

Verification

Naoya Yamashita releases lean-ritsuryo, Japanese statutory computation with proofs in Lean

The Lean 4 library and CLI (Apache-2.0 license) compute periods, deadlines, ages, holidays, and taxes under Japanese law, including income and inheritance tax. The library's functions come with proofs that they compute what the provisions say, and the CLI computes by calling them; the README also links a paper.

Checked against: conao3/lean-ritsuryo

Lean core

Sebastian Graf lets Lean's vcgen tactic discharge frame conditions with frameproc theorems

The vcgen tactic now discharges the frame condition of each framed call with a theorem named by a @[frameproc], for example one for a separation logic, so the frame condition no longer becomes a verification condition. Sebastian Graf also added the @[vcgen_simp] attribute, which collects Sym.simp theorems for vcgen.

Checked against: lean4#16093lean4#15955

AI and formalization

Researchers formalize the Strong Perfect Graph Theorem in Lean with AI agents

The complete Lean proof follows, result by result, the 2006 proof by Maria Chudnovsky, Neil Robertson, Paul Seymour and Robin Thomas that a finite graph is perfect (every induced subgraph's chromatic number equals its clique number) exactly when it is Berge (it and its complement lack induced odd cycles of length at least five).

Checked against: mahdi-jfri/StrongPerfectGraphTheorempalomar-registry.org

AI and formalization

Axiom Math formalizes the Stacks Project in Lean with AI agents

The library, Stacks, covers chapters 3 to 109 of the open-source algebraic geometry reference in over 15 million lines of code; Lean's kernel checks every proof, but only the StacksCore tier is human-reviewed. Axiom Math found several Stacks Project statements that do not hold in the generality stated and formalized corrected versions alongside counterexamples.

The Stacks Project library as a city: the chapter treemap as ground, each Lean declaration a column as tall as its dependency level, theorems in gold and propositions in red.
Image: axiommath.ai

Checked against: axiommath.aileanprover.zulipchat.comAxiomMath/Stacksstacks.axiommath.ai

AI and formalization

Fedor Popov and Leonardo Rastelli release LeanVOA, a vertex operator algebra library

The Mathlib-based library (11,660 Lean files, 3,752,244 lines) constructs the Moonshine module, formalizes Zhu's modular invariance and Huang's tensor categories, and proves new results, declaring no axiom of its own. Under the authors' direction, AI agents (Claude Opus, Claude Fable, Codex) wrote the Lean code and first drafts of a 2,337-page companion book.

Checked against: Fedor-Popov/Lean_VOAleanprover.zulipchat.com

AI and formalization

Mahdi JafariRaviz's repository formalizes a quasipolynomial-time graph isomorphism algorithm in Lean

The proof writes the whole deterministic algorithm from a paper by MohammadTaghi Hajiaghayi and Mahdi JafariRaviz as one program for a simple machine and proves it gives correct answers within the time bound. Ten results from the literature, each relying on the classification of finite simple groups, serve as axioms.

Checked against: mahdi-jfri/GraphIsomorphismLog2

AI and formalization

Scott Armstrong and Ahmed Bou-Rabee fully formalize Elboim-Sly paper with AI agents

Dor Elboim and Allan Sly proved Tóth's conjecture in five or more dimensions: the interchange process (particles swapping across lattice edges whose Poisson clocks ring), run long enough, yields a permutation with infinite cycles. Claude Opus 5.5 and Claude Sonnet 5.5 wrote the Lean code (about 180,000 lines), which assumes nothing the paper cites.

Checked against: scottnarmstrong/elboim-slypalomar-registry.org

AI and formalization

Xi Yin, Michael R. Douglas and Anna Mei machine-check the Osterwalder-Schrader correspondence

Three Lean theorems, registered in the Palomar Registry, go from Euclidean Schwinger functions to relativistic Wightman distributions and back, in every positive spatial dimension. Euclidean growth is assumed and not recovered, so the two directions do not compose to a biconditional; field operators are not reconstructed, and four conventions are weaker than textbook ones.

Checked against: palomar-registry.orgmrdouglasny/OSreconstruction-comparator

AI and formalization

Nidhal Mghirbi and Seth Douglas give Lean-checked hyperbolic counterexamples to Kaplansky's conjectures

For every prime p, a torsion-free, word-hyperbolic group based on OpenAI's constructions fails all four group-ring conjectures in characteristic p; no torsion-free hyperbolic counterexample to any of them was previously known. Nidhal Mghirbi's Lean 4 formalization proves the main theorem, including existence forms of the random-graph estimates, and builds on OpenAI's Lean development.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2611.04599Apsiape/kaplansky-conjectures-hyperbolic-groups

Verification

Luk Koska, Tom Koska and Ben Koska verify GPU kernels in Lean

The authors formalize PTX, combining an interpreter covering 81 instruction forms with the axiomatic PTX memory model, and prove correct 9 hand-written PTX entry points (454 instructions), including simple implementations of FlashAttention and a 3-kernel MoE pipeline. LLM coding agents helped write the 34,034 lines of proof, which contain no sorry or custom axioms.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2611.04447paperswithlean.com

Verification

LARK verifies GPU kernels against PyTorch references using LLM agents and Lean

LARK formalizes a GPU machine model and per-operation semantics in Lean 4 once per target language (PTX, CUDA, HIP), and agents prove segment-by-segment equivalence under exact arithmetic. Of 10 production kernels from LLM serving frameworks, it verifies 9 and finds a previously unknown data race in the tenth, an llm.c softmax kernel.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2611.02028paperswithlean.com

AI and formalization

Baoyu Zhang and Shengmin Zhang prove Díaz–Park conjecture, formalized in Lean

The conjecture concerns sharpness of saturated fusion systems; the proof avoids the classification of finite simple groups and answers a question from M. Aschbacher, R. Kessar and B. Oliver's list of important open problems. The formalization, built with AI assistance from Codex, spans Lean (61,849 lines in 957 modules) and Rocq (99,857 lines).

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2611.02043BaoyuZhang747/sharpness-Lean-Rocqpaperswithlean.com

Verification

Sreehari Sankar and coauthors present LeanGuard, Lean-verified guardrails for AI agents

LeanGuard checks every tool call an agent proposes against a Lean 4 policy, using a decision procedure proved equivalent to a LeanLTL temporal semantics. On Tau-Bench, unguarded Qwen agents executed at least 33 policy-forbidden calls while LeanGuard executed none, and it cut direct prompt-injection success on DTap from 57.9% to 5.9%.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2611.02332DebarghaG/LeanGuard

Verification

Jan Onderka, Armin Biere and Henrik Böving verify a Lean SMT-LIB parser

The paper introduces blazing-smtlib, a Rust parsing library for SMT-LIB (a standard input format for SMT solvers), and its Lean port BSmtLib, whose optimised lexer and parser provably match a formalised SMT-LIB syntax. On 9,201 benchmark files, blazing-smtlib is more than 6 times faster than previous libraries (geometric mean); BSmtLib is faster or comparable.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2611.00185onderjan/blazing-smtlibpaperswithlean.com

Papers and events

Researchers bring effect handlers to JAX, backed by Lean 4 proofs

Oghenevwogaga Ebresafe, Daniel Zheng, Gordon Plotkin, and Ningning Xie compile effect handlers to restricted, first-order accelerator languages via a translation that statically eliminates the handlers and preserves typing and semantics, with proofs fully mechanized in Lean 4. The design is implemented as a library for JAX, a Python domain-specific language for accelerator programming.

First page of the paper
Image: paperswithlean.com

Checked against: arXiv:2611.03918

More news