The construction, obtained October 28, 2026, proves a challenge statement with a Mathlib-only import closure: for each closed matrix subgroup with nonabelian simple real Lie algebra, a Wilson lattice family with a Wightman reconstruction (positive energy, unique vacuum). A kernel replay found only standard axioms; a positive mass gap is outside the challenge's scope.
Checked against: yang-mills-group/OpenAI-YM-20261028
The hairer/humanise-yang-mills repository plans a research monograph giving detailed proofs, traceable to a fixed version of the announced Lean formalisation of four-dimensional Yang-Mills theory, with contributors' agents working on tasks claimed through GitHub issues. Preliminary dependency mapping is under way; a full build, axiom audit, and line-by-line mathematical audit are still outstanding.
Checked against: hairer/humanise-yang-mills
In the Lean 4 framework by Alexander Tyurin, QuocViet Pham, Valentin Khrulkov, and Ivan Oseledets, agents such as Codex or Claude Code search for better oracle-call budgets under a fixed problem setup, and Comparator independently audits each result. One new gradient-only guarantee for (L0,L1)-smooth convex optimization resolves what the authors call an open problem.
Checked against: arXiv:2611.13872k3nfalt/longtails
AI agents (Anthropic Claude models) wrote most of the proof under the authors' supervision, and the team spent about 80,000 USD on model access and server compute. The Lean proof certifies the conjectures as stated in LeanEval; a blueprint website presents it as layered natural-language notes, unfinished in parts not directly needed for it.
Checked against: leanprover.zulipchat.comformal-arithmetic-geometry/weil-conjecturesweil-conjectures.merten.devaxiommath.ai
The conjecture says a bounded polynomial of low degree on the discrete cube has an influential variable. AI models produced the proof, paper and formalization in a research harness developed by David Turturean at PSI; the formalization has no placeholder or added axiom and was re-checked by two independent Lean kernel implementations.
Checked against: physical-superintelligence/aaronson-ambainis
The conjecture, open since 1934, says the smoothed octagon (a regular octagon with its corners cut off by hyperbola arcs) packs the plane worst among centrally symmetric convex shapes. The-Anh Vu-Le directed the work, which follows Thomas Hales's optimal control formulation; no person has checked the proof, though Lean's kernel checks every step.
Checked against: vltanh/lean4-smoothed-octagonpalomar-registry.org
The library, Weil, has about 220,000 lines of code, written by AI agents and not yet reviewed by humans; reusing Axiom Math's earlier Lean formalization of the Stacks Project, an algebraic geometry reference, let the team finish in 24 hours. The top-level theorem copies verbatim the LeanEval problem weil_conjectures, which uses only Mathlib definitions.
Checked against: axiommath.aiAxiomMath/Weilleanprover.zulipchat.com
Among four-qubit pure states, only M₄ and its complex conjugate, up to local unitaries, maximize the mean von Neumann entropy of the three balanced bipartitions; the paper also proves the Gour-Wallach conjecture for Rényi entropies. The Lean 4 and Mathlib formalization covers most four-qubit results and parts of the computer-assisted seven-qubit ones.
Checked against: arXiv:2611.05757cmbant/qubit-entropy
The Herzog-Schönheim conjecture states that if a group is partitioned into finitely many, and at least two, cosets of subgroups, then two of these subgroups have the same index. The arXiv paper proves it for all solvable groups, finite or infinite, and the proof has been formalized in Lean 4 with Mathlib.
Checked against: arXiv:2611.11002
Dömötör Pálvölgyi's heptagon and generic seven points on a circle (Theorem A.3 of arXiv:2609.23327) are proved non-Ramsey under formal-conjectures' definition, copied byte for byte (Ramsey: for any number of colours, every colouring of some Euclidean space has a monochromatic copy). Anthropic's Claude wrote the Lean proofs under Carlos Toledo's direction, building on OpenAI's formalization.
Checked against: palomar-registry.orgcarlostoledo1891/heptagon-ramsey-lean
Brouwer's theorem, in every finite dimension, has two proofs: an analytic one, following John Milnor (1978) and C. A. Rogers (1980) and using no homology, degree theory or simplicial approximation, and one through Sperner's lemma. Claude Opus 5.5 wrote the proofs in Claude Code; no person has reviewed them, and Lean has checked them.
Checked against: palomar-registry.orgvltanh/lean4-fixed-point
The release adds verified model checkers for safety (2 to 20 times faster than TLC) and liveness, an LTL proof mode, a TLA+-to-Veil LLM skill, and a PlusCal-style DSL. George Pîrlea says Veil now supports anything the TLA+ Toolbox is used for; Ilya Sergey credits @zqy1018 and external contributors.
Checked against: @ilyasergey on X@GeorgePirlea on X
David Andrews and Chao Zhang's model spans 613,318 lines of Lean with 18,898 theorems and lemmas; each modelled function must agree with the real interpreter on at least 50,000 cases. Of 26,004 functions in scope, 4,071 (15.7%) are judged faithful by independent review, and 418 bug records reproduce on 3.15.2, each with a reproducer.
Checked against: Broyojo/python-formalization
Keel, an in-kernel proof checker for the Linux eBPF verifier, is specified in Lean and proved sound against bit-vector semantics; its implementation in EmbC, a deeply embedded C fragment, is proved to refine that specification. Formalizing the eBPF Certificate Framework (BCF) checker uncovered 13 bugs, and Keel runs 1.3X faster than BCF's checker.
Checked against: arXiv:2611.11117
Built on EthLib's EVM model and program logic, the proofs are about the 11,075 deployed bytes read from Ethereum mainnet; the Solidity source served only as a guide. The README says each of its claims is proved and has passed several independent reviews, and that this does not mean USDT is verified unconditionally.
Checked against: Giulio2002/usdt-verify
The code covers field arithmetic, G1 encoding and decoding, and subgroup and pairing-product checks, specializing routines from the arkworks 0.5.0 crate; proofs establish termination and agreement with EthLib under documented preconditions, while arkworks agreement is tested and the Charon/Aeneas translation remains trusted. The project was mostly AI-generated and has not been independently reviewed.
Checked against: zksecurity/arkworks-ethlib
The project defines and proves the semantics of Verse (Epic Games' functional logic programming language) in Lean 4 and checks a C runtime against it. Its C components for integer arithmetic, program loading, and rollback are proved with QuickProof (VST and CompCert in Coq); differential testing and fuzzing check the object store and value heap.
Checked against: rudi-cilibrasi/openverse
SampLib expresses samplers from Peter Occil's articles as executable ProbLang terms and proves them correct in continuous TotalEris, building on logsem/clutch-lean and Lean 4.35.0. Its completed baseline suite contains 216 samplers, and the README notes that the interpreter tests are not proofs and that the interpreter uses finite-precision Float arithmetic.
Checked against: markusdemedeiros/SampLib
The algorithm, peta-shock conversion, propagates evaluation values recorded in a shogi AI's opening book backward from the end positions and covers books containing ordinary and perpetual-check repetitions. PaperClaims.lean links the accompanying paper's theorem numbers to Lean theorem names, and Audit.lean checks the axioms the theorems depend on.
Checked against: yaneurao/peta-shock
DBLog-based incremental snapshots, adopted by Debezium and Flink CDC, originally did not handle orphan rows (in the sink, absent at the source); the extension deletes keys a chunk read did not return. Safety and convergence are proved in Isabelle/HOL and, except for the Flink CDC theory, in Lean 4, with no unfinished proofs.
Checked against: arXiv:2611.10810doi.org
In a post on X, Jason Rute wrote that writers covering Lean's "trust surface" without mentioning external checking, comparator, and con-leche have not done the homework, and that "there is a lot of false and misleading info out there."
Checked against: @JasonRute on X
Continuous integration checks replace code review: on a zero-copy authenticated message router, the kernel check passed in 42 ms and mutation testing killed all 10 synthetic bugs. The paper builds on Lean 4 artifacts (salt, x86lean, vir) and contrasts Lean subtypes with Computational Type Theory subset types; several components remain proposals.
Checked against: arXiv:2611.02285paperswithlean.comjyh/vir
Christopher Atherfold, Maxim Gerspach and Jad Hamdan study the 2q-th moments, for q from 0 to 1, of sums up to x of a random, completely multiplicative function with independent, uniform ±1 values at the primes. A transition from better-than-square-root cancellation to growth like a power of log x occurs when q crosses 1/2.
Checked against: arXiv:2611.05492
Google DeepMind and Google Quantum AI researchers had teams of AI agents write quantum programs in a Lean library and prove both correctness and resource cost; a separate checker confirmed each solution met the original specification. The preprint reports a 290-fold reduction over prior baselines for a quantum arithmetic routine (an arcsine calculation).
Checked against: mlq.ai