What Does Lean-Checked Mean? Formal Proofs Explained

"Lean-checked" means a proof was written in the Lean proof language and accepted by Lean's kernel, a small program that re-checks every step against the definitions, earlier theorems and axioms the proof is allowed to use. It certifies the formal statement written in Lean, not the English paper around it. In OpenAI's 2026 collection of AI-generated mathematics, 242 of 372 result families have a Lean formalization. All 416 of the collection's Comparator checks allow only Lean's 3 standard axioms, and 80 of the formalization notes say part of the paper is outside the formal statement.

This page explains what a Lean check proves and what it leaves open. It walks through the four levels of checking in Lean's own guide, gives a checklist for any "Lean-verified" claim and works one result through it: #247, an infinite finitely presented periodic group. It ends with a tracker of all 372 results, read from the repository files at commit 1581d4c (2026-10-12).

What Lean is

Lean 4 is a programming language that doubles as a proof assistant. You write a theorem statement and a proof, and Lean checks that the proof really establishes the statement. Proofs are usually written with tactics, small programs such as decide, ring or simp that build the detailed proof for you. Whatever the tactics produce, the finished proof is handed to the kernel, the part of Lean that does the final check. A mistake in a tactic therefore produces an error rather than a false theorem. Lean's reference manual lists "honest bugs in meta-programs and tactics" among the things even the most basic check protects against.

Most serious work builds on Mathlib, the community library of formalized mathematics. It is the first library listed in OpenAI's formalization catalogue, which orders them by how often the project imports them.

The smallest possible example:

example : 1 + 2 = 3 := by decide   -- accepted: Lean works it out and agrees
example : 1 + 2 = 4 := by decide   -- error: the statement is false, so no proof is produced
example : 1 + 2 = 4 := by sorry    -- warning: declaration uses `sorry` (nothing is proved)

A real proof works the same way with thousands of steps instead of one. Every step must follow from what came before, or the file does not check.

sorry: the placeholder that can "prove" anything

sorry stands in for a proof you have not written yet. Lean accepts the file but warns declaration uses `sorry` (before Lean 4.28 the quotes were straight: declaration uses 'sorry'); the error page covers both. Behind the scenes sorry uses an axiom called sorryAx, which the Lean reference manual says "can be used to prove anything" and is "not intended to occur in finished proofs". A theorem that depends on sorry, directly or through anything it uses, is not proved.

The manual adds a trap worth knowing. The blue double check marks that the Lean editor shows next to a finished theorem "appear even when there are explicit uses of sorry or incomplete proofs in the dependencies". A tick next to the headline theorem is not enough on its own. You have to list its axioms, as described next.

💡One file is supposed to contain sorry: a Comparator challenge file. It states the theorem with sorry as its proof because its only job is to say what must be proved. The proof lives in a separate solution file. Seeing sorry in a challenge file is not a sign the proof is missing.

Axioms: what a proof is allowed to assume

Every proof rests on axioms, statements accepted without proof. Running #print axioms theoremName lists every axiom a theorem depends on, including through the theorems it uses. The Lean reference manual says how to read the list:

Axiom reported by #print axioms	What it means
`propext`, `Quot.sound`, `Classical.choice`	The 3 standard axioms of Lean's logic: propositional extensionality, the quotient construction and a choice principle. The manual calls them "benign".
`sorryAx`	The theorem or something it depends on uses `sorry` or is otherwise incomplete. Not proved.
A name containing `_native`	Native evaluation was used (for example by `native_decide`), so the proof also trusts Lean's compiler, not just the kernel.
Any other name	A custom axiom declared by the author. The theorem is only valid if that axiom is true.

The part no checker does: does the statement say what the paper says?

Lean's guide separates two questions: "does the theorem have a valid proof" and "what does the theorem statement mean". The kernel answers only the first. If a definition in the statement is subtly wrong, Lean will faithfully verify a proof of the wrong thing. The guide warns that a statement's referenced definitions "must be investigated carefully, in particular with regard to custom notation and type classes."

The Comparator documentation gives a blunt example. Suppose a challenge leaves a definition open for the solver to fill in (a definition hole) and asks for a proof that RiemannHypothesis ↔ ChallengeSolution. A solver could define ChallengeSolution as RiemannHypothesis itself and prove the equivalence in one line, which settles nothing. Comparator's rule is that definition-hole solutions "must always be checked with an additional (potentially human) verifier." In OpenAI's collection, 9 results use definition holes. One is #158, "The Euclidean plane cannot be colored with five colors", whose check leaves the meaning of ProperColoring to the solution.

The other gap is scope: a formal statement often covers only part of a paper. Two examples from OpenAI's own notes:

#179, circulant Hadamard and Barker sequences. The circulant Hadamard classification (orders 1 and 4 only) is formalized, and so are the even Barker lengths (2 and 4). The odd Barker lengths are "outside this selected additional statement".
#017, the irrationality exponent of π is 2. The exponent is formalized; the paper's consequence for the Flint–Hills series is outside it.

Lean's four levels of checking

The Lean reference manual's chapter "Validating a Lean Proof" sets out an escalating series of checks. Each one also catches everything the levels above it catch:

Level	What you do	What it adds
1. Blue check marks	See the double tick in the editor, or run `lake build` with no errors or warnings	Catches incomplete proofs, an explicit `sorry` in the theorem itself and honest tactic bugs
2. Print axioms	`#print axioms` and confirm only the 3 standard axioms appear	Catches `sorry` and incomplete proofs in dependencies, and custom axioms
3. lean4checker	`lean4checker --fresh` on the built module	Replays the stored proofs through the kernel; catches bugs in Lean's handling of the kernel's state, and meta-programs that bypass it
4. Gold standard	Judge the proof with Comparator, external checkers enabled	Sandboxed build, statement matched against a trusted challenge; catches deliberately misleading proofs and bugs not shared by every checker

The guide reserves the gold standard for "high risk scenarios (proof marketplaces, high-reward proof competitions, unaligned AI)". Its definition of a possibly malicious proof explicitly "includes un-reviewed AI-generated proofs and programs". Even the gold standard still assumes the soundness of Lean's logic, a correct Comparator, a secure sandbox, no bug shared by every checker and "no human error or misleading presentation of the theorem statement in the trusted challenge file."

How a Comparator check works

Comparator, from the Lean developers, is "a trustworthy judge for Lean proofs". A check has three parts:

A challenge file, written by someone you trust, that states each theorem (with sorry as its proof) and every definition the statement uses.
A solution file from whoever claims the proof, restating the same theorem with a real proof.
A small JSON config naming the theorems, the permitted axioms, any definition holes and any extra kernels.

Comparator builds the solution in a sandbox and exports the finished proofs. It then re-checks them outside the sandbox. If it succeeds, each listed theorem is guaranteed to prove the same statement as the challenge, use no axioms beyond the permitted list, and be accepted by the Lean kernel. Comparator can also run nanoda, an independent kernel written in Rust, so that a bug in one kernel is not enough to pass.

OpenAI publishes 416 such configs. All of them permit exactly propext, Quot.sound and Classical.choice. 2 results enable the second kernel; the rest rely on Lean's kernel alone, one step short of the guide's gold standard. Anyone can add nanoda when re-running them.

Worked example: #247, an infinite finitely presented periodic group

The finitely presented Burnside question asks whether a group built from finitely many generators and relations, in which every element has finite order, must be finite. OpenAI's paper of 23 September 2026 says no. It builds a counterexample: a Steinberg group, St₁₂(R), over an algebra R of characteristic two. Here is the end of the challenge file lean/ComparatorChallenges/PeriodicGroup.lean, quoted from the repository (Apache-2.0):

def Periodic (G : Type u) [Group G] : Prop := ∀ g : G, ∃ m : ℕ, 0 < m ∧ g ^ m = 1

def BurnsideStatement : Prop :=
  ∃ (G : Type) (_ : Group G), Infinite G ∧ Group.IsFinitelyPresented G ∧ Periodic G

theorem thm_main : MainStatement ∧ BurnsideStatement := by
  sorry

Running it through the checklist below:

The statement says what the paper claims. BurnsideStatement asks for a group that is infinite, finitely presented and periodic. Infinite and Group.IsFinitelyPresented come from Mathlib. Periodic is defined right in the file, in one line: every element g has some m > 0 with g^m = 1. That matches the scope note: "each element has some finite order; no common exponent is asserted." MainStatement pins the witness to the Steinberg group St₁₂(R) over an algebra over ZMod 2.
The sorry is expected. This is the challenge. The proof is the solution module OAI.GroupTheory.PeriodicGroups.Main, where thm_main is stated again with a proof. Comparator's job is to confirm the two statements match.
Axioms. The config PeriodicGroup.json permits only the 3 standard axioms.
Definition holes. None: definition_names is empty, so every definition in the statement is fixed in the challenge.
Kernels. enable_nanoda is false, so the published check uses Lean's kernel only.
Scope. The note covers the periodic-group result. It says the paper's "separate nil-algebra and radical-algebra conclusions are outside these selected statements". The family's title also names a 5 October companion paper (a residually finite 2-group). The scope note links only the 23 September paper, and "residually finite" does not appear in the formal statement.
Reproduction and review. The repository publishes the check, not a log of an independent re-run. Its formalization catalogue lists the review status as "unchecked".

Verdict: this is a well-specified, checkable claim. The statement is short enough to read in full, it has no definition holes and it uses only standard axioms. The main Burnside result is as solid as a Comparator run makes it. The companion paper and the algebra conclusions are not covered by this check.

A checklist for any "Lean-verified" claim

Find the formal statement. No Lean file, no Lean check. "Formalization in progress" is not a check.
Read the statement and every definition it uses. Look for definitions written in the same file, custom notation and anything that makes the claim weaker than the paper's.
Look for definition holes. If the solver gets to define part of the statement, a person has to confirm the definition means what it should.
Search for sorry in the proof and everything it imports from the project (the challenge file excepted).
Print the axioms. Only propext, Quot.sound and Classical.choice should appear.
Check which kernels ran. Lean's kernel alone, or a second independent checker such as nanoda as well.
Check the scope. Which of the paper's theorems are formalized and which are "outside the selected statement"?
Check it was re-run. A published config shows how to check the claim. Someone still has to run it, ideally someone other than the author.
Check human review. Has a mathematician confirmed that the formal statement matches the published claim?

Verification tracker: all 372 OpenAI results

Each row is one result family from github.com/openai/math, read by script from the repository at commit 1581d4c (2026-10-12). Titles link to the Lean scope note where one exists, otherwise to the first paper.

372result families (719 papers)

242with a Lean formalization

80formalize only part of the paper

9with definition holes

4check a supporting result only

2with a second kernel

How to read the columns: Lean: Yes means the repository has a scope note and published Comparator checks for that result; it does not mean we re-ran them. Part of the paper not formalized is our reading of the scope note's wording, so follow the link for the exact text. Supporting result only marks checks the repository says "verify supporting results, not the corresponding papers' main theorems". A row with no Lean formalization is the model's claim alone; the README itself warns that "some of the unformalized results could have issues."

#	Result family	Lean	Notes
001	Milne’s rationality conjecture and algebraic specialization	No	–
002	The full BSD formula from low Selmer corank	No	3 papers
003	The quasi-Riemann hypothesis	Yes (4 checks)	Part of the paper not formalized; 3 papers
004	Hilbert’s tenth problem over ℚ	No	2 papers
005	Irrationality of Catalan’s constant	Yes	–
006	Goldfeld’s conjecture: densities and mean analytic rank	No	2 papers
007	Ordinary two-point correlations and the corrected Elliott conjecture	Yes (2 checks)	–
008	The Deligne–Drinfeld conjecture	Yes	Part of the paper not formalized
009	Function-field reconstruction from Milnor K-theory and Galois data	Yes	Part of the paper not formalized; 3 papers
010	Unrestricted pro-modularity at the prime two	No	3 papers
011	Prime-factor statistics of p − 1	No	3 papers
012	Independent largest prime factors of consecutive integers	Yes	–
013	Ostmann’s inverse Goldbach conjecture	Yes (2 checks)	–
014	Restricted geometric Langlands, global Arthur enhancements, and generic Ramanujan	No	8 papers
015	Torus-packet equidistribution in prime, quartic, and sextic degrees	Yes	3 papers
016	Zilber–Pink in abelian varieties and the Siegel threefold	No	4 papers
017	The irrationality exponent of π is 2	Yes	Part of the paper not formalized
018	The Margulis–Platonov conjecture over global fields	No	2 papers
019	The local p-adic section conjecture and global consequences	No	2 papers
020	Squarefree quartics and power-free polynomial values	Yes	–
021	A quadratic bound for Jacobsthal’s function	Yes (2 checks)	–
022	The weak inhomogeneous Duffin–Schaeffer conjecture	No	–
023	Patterson's first moment for cubic Gauss sums	Yes	–
024	An asymptotic formula for the number of totients	Yes (2 checks)	–
025	Short Egyptian fractions	Yes (2 checks)	–
026	Positive lower density of large prime gaps	Yes	–
027	Potential integral density on curve character varieties	Yes	Supporting result only; Part of the paper not formalized
028	Uniformly bounded components of Gaussian-prime graphs	Yes	–
029	Primitive roots for every admissible integer base	No	2 papers
030	Modularity of elliptic curves over imaginary quadratic fields	No	–
031	Uchida’s conjecture for open homomorphisms of Galois groups	No	–
032	The rational Hodge conjecture for CM abelian varieties	No	5 papers
033	Iitaka subadditivity, variation, and logarithmic additivity	Yes	Part of the paper not formalized; 5 papers
034	Log abundance for compact Kähler spaces under logarithmic Iitaka subadditivity	No	14 papers
035	Log-canonical threefold abundance in numerical dimension one	No	2 papers
036	Numerical semiampleness and generalized minimal models	No	4 papers
037	The ordinary-double-point volume gap	No	2 papers
038	Fujita’s freeness conjecture	No	–
039	Nagata’s conjecture and maximal Seshadri constants	Yes (2 checks)	4 papers
040	Bloch’s conjecture for complex surfaces	No	–
041	Hyperkähler SYZ and projective-space bases	No	2 papers
042	Oka classification for minimal compact complex surfaces: Kodaira dimension zero and class VII	No	–
043	P = W for fixed-determinant SL_n moduli spaces	No	–
044	The equivariant cohomological Hikita conjecture	No	–
046	Shafarevich counterexamples in dimension two and with large fundamental group	No	2 papers
047	Zariski cancellation and affine fibrations over the complex numbers	Yes	Part of the paper not formalized
048	A characteristic-zero counterexample to Lipman–Zariski	No	–
049	A stable-coordinate counterexample in four variables	Yes (3 checks)	2 papers
050	A counterexample to Griffiths’ positivity conjecture	Yes	Part of the paper not formalized
051	Kobayashi’s canonical-ampleness conjecture	No	–
052	Tangent splittings and product decompositions	Yes (2 checks)	Part of the paper not formalized; 2 papers
053	A counterexample to Pixton completeness in Chow	No	–
054	Irrational cubic fourfolds with Hodge-theoretic and categorical K3 associations	No	–
055	Gepner symmetry and large-volume stability on threefolds	No	2 papers
056	Termination of projective and Kähler fourfold minimal model programs	No	5 papers
057	Fundamental groups of special complex varieties and root orbifolds	No	3 papers
058	Semialgebraic universal covers and bounded domains	Yes	2 papers
059	Counterexamples to Zariski’s multiplicity conjecture	No	2 papers
060	The Global Spherical Shell conjecture	No	–
062	Projective contact classification and the LeBrun–Salamon conjecture	No	–
063	The generalized Mukai conjecture	No	–
064	Topological triviality of μ-constant surface singularities	No	–
065	Virasoro constraints for complete intersections and projective-bundle towers	No	2 papers
066	Bounded klt complements for Fano contractions	Yes	Supporting result only; Part of the paper not formalized; 2 papers
067	The Campana–Peternell conjecture in dimension six	No	–
068	Anticanonical nonvanishing in every dimension	No	7 papers
069	Global quantum geometric Langlands at irrational level	No	–
071	Koebe’s circle-domain conjecture	Yes	2 papers
072	Brennan's conjecture and the integral-means spectrum	Yes (3 checks)	2 papers
073	The Falconer distance conjecture	Yes (2 checks)	–
074	Kakeya in three and four dimensions	No	2 papers
075	The L log L Fourier-convergence conjecture	Yes	–
076	Real ultraflat Littlewood polynomials and unbounded binary merit factors	Yes (2 checks)	3 papers
077	Fourier restriction for positively curved surfaces	No	2 papers
078	The three-dimensional Bochner–Riesz conjecture	No	–
079	Local smoothing in three dimensions	No	–
080	The exact Sobolev endpoint for Schrödinger convergence	No	2 papers
081	Riesz transforms and rectifiability in higher codimension	Yes	Part of the paper not formalized
082	Annular variation and dyadic absolute bounds for the triangular Hilbert transform	Yes	3 papers
083	Hilbert transforms along Lipschitz directions	Yes	–
084	The geometric case of the Erdős similarity conjecture	Yes	2 papers
085	Endpoint Sobolev regularity of centered disk averages	Yes (2 checks)	Part of the paper not formalized
086	An L³ bound for the trilinear Hilbert transform	No	–
087	The Mahler conjectures, functional inequalities and polar-product symplectic width	Yes (4 checks)	Part of the paper not formalized; 3 papers
088	Sharp projection-body inequalities and a counterexample to simplex maximization	Yes (3 checks)	Part of the paper not formalized; 2 papers
089	Bounded-distortion L₁ embeddings of planar and bounded-treewidth graphs	Yes (2 checks)	2 papers
090	Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy	Yes (4 checks)	Part of the paper not formalized; 4 papers
091	Logarithmic and L_p Brunn–Minkowski inequalities and the B-conjecture	Yes	–
092	The optimal order of convex-body covering density	Yes (2 checks)	2 papers
093	Dimension-free logarithmic Sobolev inequality for subgaussian log-concave measures	No	–
094	Subpolynomial dimension reduction in L_p	Yes	–
095	Hyperbolicity cones without semidefinite lifts	Yes	3 papers
096	The Gaussian propeller conjecture in every dimension	Yes	Part of the paper not formalized
097	The Euclidean Steinitz–Bergström bound	Yes	–
098	Compact counterexamples to bi-Lipschitz dimension reduction	Yes (2 checks)	–
099	The sharp exponential scale of edit-distance distortion	Yes (4 checks)	Part of the paper not formalized; 3 papers
100	Cylinder coverings below the half-area bound	Yes (3 checks)	Part of the paper not formalized; 4 papers
101	The sharp simplex conjecture for isotropic constants	No	–
102	The Unique Games Conjecture and optimal approximation thresholds	Yes (5 checks)	5 papers
103	Exact derandomization of logarithmic space: L = RL = BPL	Yes	Definition holes: needs a human check
104	Quasipolynomial algorithms for mean-payoff, stochastic and parity games	Yes (2 checks)	4 papers
105	Perfect completeness for 2-to-1 games	Yes	–
106	Hardness of coloring three-colorable graphs	Yes	–
107	Matrix multiplication with exponent at most 9/4	Yes (2 checks)	3 papers
108	A cubic permanent–determinant lower bound	Yes (2 checks)	Part of the paper not formalized
109	Integer multiplication below n log n	No	–
110	Optimal-order randomized k-server on arbitrary metrics	Yes (2 checks)	Definition holes: needs a human check; 2 papers
111	One-sample matroid prophet inequalities against an almighty adversary	Yes (2 checks)	–
112	Beyond the square-root exponent for depth-three circuits	Yes	–
113	Approximate counting and entropy of perfect matchings	Yes (6 checks)	Part of the paper not formalized; 2 papers
114	Approximate counting of common integer polymatroid bases	Yes	2 papers
115	Sampling and counting contingency tables with arbitrary margins	Yes	2 papers
116	Uniform black-box noncommutative identity testing across characteristics	Yes (2 checks)	3 papers
117	Uniform sparsest cut: hardness and semidefinite gaps	Yes	2 papers
118	Bin packing and unbounded configuration-LP gaps	Yes	–
119	The Courtade–Kumar and Hellinger conjectures	Yes (2 checks)	2 papers
120	Almost-linear-time exact matching and prescribed-degree factors in general graphs	No	–
121	Almost-linear approximation of edit distance	Yes	–
122	Quantitative trace-reconstruction bounds with a uniform decoder	Yes	3 papers
124	Polynomial-time scheduling on three identical machines	Yes	–
125	The metric k-median approximation threshold and recovery	Yes (4 checks)	2 papers
126	Exponential semidefinite complexity of perfect matching	Yes (2 checks)	–
127	Average sensitivity of polynomial threshold functions	Yes	–
128	A factor-two approximation for shortest common superstring	Yes	–
129	Exponential state costs for two-way automata	Yes (3 checks)	Part of the paper not formalized; 2 papers
130	Exact Fourier transforms below n log n	Yes (2 checks)	Part of the paper not formalized; 2 papers
131	Rapid mixing of graph switches for every degree sequence	Yes	Part of the paper not formalized
132	A superquadratic separation of sensitivity and block sensitivity	Yes	–
133	The computational complexity of Weisfeiler–Leman refinement	Yes (4 checks)	Part of the paper not formalized; 4 papers
134	Generalized star height at most three	Yes	3 papers
135	Homogeneous depth-five lower bounds for iterated matrix multiplication	Yes	–
136	A quasilinear PCP theorem for PPAD	No	–
137	One-tape time simulation in two-fifths-power space	Yes	Part of the paper not formalized
138	Subset Sum in O(2^0.49n) time	No	2 papers
139	Subpolynomial query complexity for log-concave sampling	Yes	–
140	Memory–sample lower bounds for noiseless Gaussian regression	Yes (8 checks)	Part of the paper not formalized; 6 papers
141	Existential–universal real sentences in the counting hierarchy	No	–
142	Deterministic polynomial factorization over prime fields	No	–
143	Hilbert's sixteenth problem: uniform bounds for limit cycles	Yes	2 papers
144	Banach’s simple Lebesgue-spectrum problem	Yes	–
145	Rokhlin’s multiple-mixing problem	Yes	Definition holes: needs a human check
146	Positive metric entropy for the standard map	Yes (3 checks)	–
147	The near-boundary Birkhoff conjecture	No	2 papers
148	The entropy-rate dimension formula for self-similar measures	Yes (2 checks)	Part of the paper not formalized
149	Classwise permanence for weakly reversible mass-action systems	Yes	2 papers
150	Weak mixing of triangular billiards with an irrational angle	Yes	2 papers
151	A C¹ counterexample to the entropy conjecture	Yes	–
152	Zero entropy does not guarantee a smooth positive-volume model	Yes	Part of the paper not formalized
153	Arithmetic classification and non-Pisot singularity for Bernoulli convolutions	No	–
154	Pointwise multiple ergodic averages for mixing transformations	No	4 papers
155	A counterexample to periodic tiling in dimension three	Yes	–
156	Borsuk's conjecture fails in dimension nine	Yes	–
157	Graph coloring, clique minors, and Colin de Verdière invariants	Yes (2 checks)	Part of the paper not formalized; 3 papers
158	The Euclidean plane cannot be colored with five colors	Yes (2 checks)	Definition holes: needs a human check
159	Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi bounds	Yes	Part of the paper not formalized
160	Superexponential van der Waerden numbers	Yes	Part of the paper not formalized
161	Counterexamples to Sidorenko’s conjecture and the forcing conjecture	Yes	Part of the paper not formalized
162	Counterexamples to Ryser’s covering conjecture	Yes (3 checks)	2 papers
164	Hindman’s finite sums and products conjecture	No	–
165	The Harary–Hill and Zarankiewicz crossing-number formulas	Yes (2 checks)	2 papers
166	The higher-dimensional Erdős distinct-distances conjecture	No	–
167	Planar distinct distances and unit-distance bounds	Yes (2 checks)	Part of the paper not formalized; 2 papers
168	Combinatorial invariance of Kazhdan–Lusztig polynomials	Yes	–
169	Shareshian–Wachs elementary positivity	Yes	Definition holes: needs a human check
170	Sharp logarithmic exponents for off-diagonal Ramsey numbers	Yes (2 checks)	2 papers
171	The hypercube Ramsey conjecture	No	–
172	Classification of finite Euclidean Ramsey configurations	Yes (7 checks)	–
173	Seymour’s second-neighborhood conjecture	Yes	–
174	Deterministic construction of strong thin spanning trees	Yes (2 checks)	2 papers
175	Talagrand’s expectation thresholds, discrete convexity, and graph decompositions	Yes (2 checks)	3 papers
176	The second Kahn–Kalai conjecture with an edge-count bound	Yes	–
177	Bounded-degree coboundary expanders	Yes	–
178	Deterministic nonbipartite Ramanujan graphs in every fixed degree	No	–
179	The circulant Hadamard and Barker-sequence conjectures	Yes (2 checks)	Part of the paper not formalized
180	Barnette’s Hamiltonian-cycle conjecture	Yes	–
181	The Erdős–Gallai cycle-decomposition conjecture	Yes	–
182	Power savings for intersective polynomial differences and prime arguments	Yes	3 papers
183	Power savings for planar halving lines and k-sets	Yes	–
184	Correspondence coloring with a fixed forbidden subgraph	Yes	2 papers
185	Counterexamples to infinite matroid intersection and packing/covering	Yes (2 checks)	–
186	Uniform influence and sharp thresholds for graph and hypergraph properties	Yes	2 papers
187	Snaky in 21 Maker moves	Yes (3 checks)	–
188	The sharp terminal leave in random triangle removal	Yes	–
189	Cycle–clique Ramsey numbers	Yes	–
190	Polynomial removal fails for ordered binary matrices	Yes	–
191	A power improvement in the Heilbronn triangle lower bound	Yes	–
192	Boolean functions violate the square-root degree bound by arbitrary factors	Yes	–
193	Serre’s intersection-multiplicity conjecture	No	–
194	Lech’s multiplicity conjecture	Yes	Part of the paper not formalized
195	A counterexample to the small Cohen–Macaulay module conjecture	Yes	Supporting result only
196	A counterexample to Kaplansky’s zero-divisor conjecture	Yes	–
197	A torsion-free group algebra that is not directly finite	Yes (4 checks)	Part of the paper not formalized; 4 papers
198	A counterexample to finitistic-dimension finiteness	Yes (2 checks)	–
199	Counterexamples to Auslander–Reiten, Tachikawa and related homological conjectures	Yes (2 checks)	Part of the paper not formalized; 2 papers
200	Eisenbud–Green–Harris and lex-plus-powers	No	2 papers
201	A counterexample to Kurosh’s division-ring problem	No	–
202	The blockwise Alperin weight conjecture	No	–
203	Donovan's conjecture over fields and complete mixed-characteristic DVRs	No	2 papers
204	Tensor saturation for even spin groups	No	–
205	Saxl’s conjecture and universal tensor squares	Yes (2 checks)	Part of the paper not formalized; 2 papers
206	Finite lattice representation and undecidability	Yes	Part of the paper not formalized; 2 papers
207	The ℓ¹-Bass conjecture for all discrete groups	Yes (2 checks)	2 papers
208	Finite symmetric tensor categories and the Verlinde tower	No	–
209	Integral counterexamples to Gersten’s conjecture	No	2 papers
210	Foulkes' conjecture for sixth powers and quadratic stabilization	Yes	Part of the paper not formalized; 2 papers
211	The geometric phase diagram, diffusion, and spectra of random planar maps	Yes	7 papers
212	Planar first-passage geometry and the absence of bigeodesics	Yes (2 checks)	Part of the paper not formalized; 2 papers
213	Critical percolation on every quasi-transitive graph	Yes (2 checks)	2 papers
214	The Benjamini–Schramm nonuniqueness conjecture	Yes (2 checks)	–
215	Canonical O(3) continuum limit and exact O(4) mass asymptotics	Yes	Part of the paper not formalized; 5 papers
216	Critical and near-critical XY scaling and BKT universality	No	6 papers
217	The low-temperature Sherrington–Kirkpatrick fluctuation law	No	2 papers
218	Conformal universality for weakly interacting and random-bond Ising models	Yes	Part of the paper not formalized; 6 papers
219	GOE bulk universality for regular graphs with weak Anderson disorder	No	2 papers
220	Directional zero–one laws beyond iid environments and iid ballisticity	Yes (3 checks)	3 papers
221	The Mézard–Parisi formula for diluted spin glasses	Yes	–
222	Perceptron free energies and microscopic jamming exponents	Yes (3 checks)	4 papers
223	Random-cluster interfaces: critical, disordered, thermal, and natural-time scaling	No	6 papers
224	Critical and quenched near-critical universality for Poisson–Voronoi percolation	No	3 papers
225	Gaussian free field limits throughout the balanced six-vertex regime	No	–
226	The double-dimer loop ensemble converges to CLE₄	No	–
227	Critical SK autocorrelation processes and dynamics across the temperature transition	Yes (5 checks)	Part of the paper not formalized; 8 papers
228	Continuum phase transitions for radial pair potentials	Yes (3 checks)	2 papers
229	Exact three- and four-state reconstruction thresholds and four-state tree capacity	Yes (2 checks)	Part of the paper not formalized; 3 papers
230	Exact Hausdorff gauges for SLE	Yes	2 papers
231	The free uniform spanning forest is a factor of IID	Yes (2 checks)	–
232	Gaussian fields and interfaces for triangular-lattice Lipschitz heights	No	3 papers
233	The joint critical Ashkin–Teller current limit	No	–
234	All-temperature pressure of orthogonally invariant Ising spin glasses	Yes	–
235	Limiting random SAT thresholds, sharp variance and computability	Yes (4 checks)	4 papers
236	The exact factor-of-IID threshold for free Ising spins on trees	Yes	Part of the paper not formalized
237	The three-quarter exponent for honeycomb self-avoiding walk	Yes (4 checks)	Part of the paper not formalized; 13 papers
238	Optimal logarithmic mixing of the Thorp shuffle	Yes (13 checks)	Part of the paper not formalized; Definition holes: needs a human check; 12 papers
239	Sharp singularity rates for symmetric random sign matrices	No	2 papers
240	Shelah's eventual categoricity and the prescribed-threshold obstruction	Yes	Part of the paper not formalized; 2 papers
241	Rigidity of the Turing degrees	Yes	Part of the paper not formalized
242	Single-fold Diophantine representations and undecidability under an at-most-one-solution promise	Yes	–
243	Separating choiceless counting from polynomial time and witnessed choice	Yes (2 checks)	Part of the paper not formalized; 2 papers
244	The Partition Principle does not imply Choice	Yes (2 checks)	Part of the paper not formalized
245	Weak normalization implies strong normalization in pure type systems	Yes	–
246	Cannon's conjecture	Yes	–
247	An infinite finitely presented residually finite 2-group and a finitely presented nil algebra	Yes	Part of the paper not formalized; 2 papers
248	Thompson's group F is nonamenable	Yes	–
249	A finitely generated Eilenberg–Ganea counterexample	Yes	–
250	Boone–Higman embeddings with higher finiteness	Yes (3 checks)	Part of the paper not formalized; 3 papers
251	Amenability, unitarizability, and strong Ulam stability	Yes (2 checks)	2 papers
252	A torsion-free hyperbolic group that is neither residually finite nor linear over any field	Yes	–
253	An infinite finitely presented simple amenable group	Yes	Part of the paper not formalized
254	Classifying spaces and geometric obstructions for Artin groups	Yes (3 checks)	Part of the paper not formalized; Second kernel (nanoda); 3 papers
255	Quasi-isometric recognition of virtually polycyclic groups	Yes	–
256	Nonsingular systems of equations over arbitrary groups	Yes	2 papers
257	A hyperbolic group without a geometric CAT(0) action	Yes	Part of the paper not formalized
258	Gersten’s conjecture and virtual compact specialness of one-relator groups	No	2 papers
259	A group without fixed price	No	–
260	Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions	Yes	Part of the paper not formalized; 13 papers
261	Localization and delocalization in the Anderson model	Yes	2 papers
262	Sharp finite-matrix Lieb–Thirring inequalities and all equality cases	Yes	3 papers
263	The ionization and generalized ionization conjectures	Yes (2 checks)	Part of the paper not formalized; 3 papers
264	Strong cosmic censorship near two-ended Kerr data	No	3 papers
265	Area laws and tensor networks for two-dimensional gapped systems	No	2 papers
266	Exactly three mutually unbiased bases in dimension six	Yes (2 checks)	Part of the paper not formalized; 2 papers
267	Positive-temperature Bose–Einstein condensation and exact quantum depletion	Yes	5 papers
268	The spin-one Haldane gap	No	2 papers
269	Uniform Laughlin gap and stability under bounded scalar disorder	Yes (4 checks)	Part of the paper not formalized; 2 papers
270	Threshold and positive-energy bound states of the BFSS matrix model	No	2 papers
271	Bloch's law, its lattice correction, and the spherical magnetization law	Yes	4 papers
272	Entanglement without distillable secret key	Yes (2 checks)	Part of the paper not formalized
273	The entropy photon-number inequality	Yes	Part of the paper not formalized
274	Parity is not in QAC⁰	Yes (2 checks)	2 papers
275	QMA-hardness of continuum Coulomb energy	Yes	2 papers
276	Classical capacity of generalized amplitude damping	Yes	Part of the paper not formalized
277	Threshold repetition for entangled games	Yes	Part of the paper not formalized
278	Failure of Kohn–Sham ensemble representation	No	–
279	Exact quantum factoring over a fixed finite gate set	Yes	–
280	Unitary vertex operator algebras and conformal nets	Yes	–
281	QAOA attains the SK optimum in the thermodynamic-first limit	Yes (2 checks)	2 papers
282	From scale symmetry to local conformal symmetry in four-dimensional QFT	No	–
283	Polynomial-time unitary synthesis from a Boolean oracle	No	–
284	The optimal quartic separation between randomized and quantum queries	No	–
285	Counterexamples to Baum–Connes and Kadison–Kaplansky	No	3 papers
286	Rigidity and arithmetic of lattice von Neumann algebras	No	2 papers
287	Isomorphism of the free group factors	Yes	–
288	Kadison's similarity conjecture	Yes (2 checks)	–
289	Strong Kadison–Kastler stability and its spatial boundaries	Yes	3 papers
290	Relative bicentralizers and modular spectral recovery	Yes	Part of the paper not formalized; 2 papers
291	Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stability	Yes	4 papers
292	Kirchberg's 𝒪₂ norm-ultrapower embedding problem	Yes	–
293	Invariant projections, hyperinvariant subspaces, and transitive algebras	Yes (6 checks)	2 papers
294	Kaplansky's quasitrace conjecture and failure of tensor-product stable finiteness	Yes (2 checks)	–
295	The Kadison–Ringrose cohomology conjecture	Yes	Part of the paper not formalized
296	The generator problem for finite factors	Yes (2 checks)	–
297	A ZFC counterexample to Naimark's problem	Yes	Definition holes: needs a human check
298	Two notions of free entropy differ even when both are finite	Yes	–
299	The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stability	Yes	–
300	Approximation and quadratic strong-operator paving	No	2 papers
301	Trace cones and Razak–Jacelon stabilization	Yes	Supporting result only; Part of the paper not formalized; Second kernel (nanoda)
302	Radius of comparison equals half the mean dimension	No	2 papers
303	Weak pure infiniteness and Cuntz-algebra absorption	Yes (2 checks)	–
304	The Hilbert–Smith conjecture in every dimension	No	–
305	Four-dimensional disk embedding and Wall's conjecture	No	3 papers
306	The purely cosmetic surgery conjecture	No	–
307	Failure of rational injectivity for maximal coarse assembly	Yes	2 papers
308	Finite Smith–Toda complexes at every height	No	2 papers
309	The Kervaire invariant problem at the prime three	No	–
310	Quillen's conjecture in rational homology	No	–
311	The Hovey–Strickland and Chai conjectures	No	–
312	The Grothendieck homotopy hypothesis	Yes	Part of the paper not formalized
313	Finite generation for the K(n)-local sphere	No	–
314	Cyclic length and chromatic fixed-point loss	No	–
315	The four-dimensional Singer conjecture	No	–
316	Curtis’s conjecture	No	–
317	Thomason model structures in all strict higher dimensions	Yes	–
318	Chromatic splitting: filtrations and counterexamples	No	5 papers
319	Counterexamples to finite generation at chromatic height two	No	–
320	Nonhomeomorphic closed aspherical four-manifolds	No	–
321	A counterexample to Wall's finite D(2) problem	No	–
322	Tingley’s sphere-isometry problem	Yes	–
323	Independence of the separable quotient problem	Yes	Part of the paper not formalized
324	Lipschitz equivalent Banach spaces need not be linearly isomorphic	Yes (2 checks)	2 papers
325	The complete Crouzeix conjecture	Yes (5 checks)	2 papers
326	The cotype–cotype conjecture under the approximation property	Yes	–
327	Markov type characterizes superreflexivity	Yes	–
328	Nonexpansive fixed points in reflexive Banach spaces	Yes	–
329	A counterexample to metric-entropy duality	Yes	–
330	A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces	Yes (2 checks)	–
331	Reflexive midpoint convexity and diamond distortion	Yes (7 checks)	Part of the paper not formalized; 7 papers
332	Metric Markov cotype of ℓ₁ and Hilbert-space Lipschitz extension	No	–
333	Smooth isometric immersions of surfaces into ℝ⁴	Yes	–
334	A smooth surface metric with no local isometric immersion in ℝ³	Yes	–
335	Gromov’s integral scalar-curvature bound for simplicial volume	No	2 papers
336	Spectral scalar curvature, Urysohn width, and macroscopic dimension	No	3 papers
337	Sharp Cartan–Hadamard isoperimetry and rigidity	Yes (2 checks)	2 papers
338	Yau's uniformization conjecture	No	–
339	Katok's entropy rigidity conjecture	No	–
340	A counterexample to the nearby Lagrangian conjecture	No	–
341	Donaldson's hypersymplectic deformation conjecture	No	–
342	Donaldson's tamed-to-compatible conjecture	Yes	–
343	Symplectic ball packing in higher dimensions	Yes (2 checks)	–
344	The metric Blaschke conjecture	No	–
345	Infinitely many closed geodesics on Riemannian spheres and closed three-manifolds	No	–
346	Sharp singular-set bounds for stationary integral varifolds	No	2 papers
347	Counterexamples to stable-Morse and strong Arnold fixed-point bounds	Yes	Part of the paper not formalized; 5 papers
348	Nonnegative-curvature Einstein classification and an L² topological gap	Yes	3 papers
349	The Solomon–Yau least-volume conjecture	No	–
350	Yau’s nodal bounds: surfaces and higher dimensions	Yes (3 checks)	3 papers
351	Scalar curvature and finite-time Ricci-flow singularities	No	3 papers
352	A finite-time singularity of Calabi flow	No	–
353	Affine Bernstein rigidity through dimension nine and a smooth dimension-ten counterexample	Yes	Part of the paper not formalized; 2 papers
354	The isoperimetric profile of the cubic three-torus	Yes	–
355	Unique tangent flows at the first surface singularity	No	–
356	Gigli’s characterization of Alexandrov curvature	Yes	2 papers
357	Bi-Lipschitz coordinates at every regular RCD point	No	–
358	A three-manifold without conjugate points or nonpositive curvature	Yes	Part of the paper not formalized
359	Negative Kähler curvature without bounded holomorphic coordinates	Yes	2 papers
360	Weak MTW curvature gives convexity and regular optimal transport	Yes (2 checks)	2 papers
361	Failure of integer-degree harmonic dimension comparison	Yes	Part of the paper not formalized; 2 papers
362	Global smoothness for relativistic Vlasov–Maxwell	Yes	–
363	Nonuniqueness with local conservation for the hard-sphere Boltzmann equation	Yes	Part of the paper not formalized; 2 papers
364	Kinetic limits and fluctuations over the Boltzmann lifespan	No	2 papers
365	Joint metric and connection recovery from one boundary patch	Yes	3 papers
366	The planar Mumford–Shah regularity conjecture and local weak-L⁴ gradient bounds	No	–
367	The critical dimension for the one-phase Bernoulli problem	Yes	Part of the paper not formalized
368	The three-dimensional Ball–Evans approximation problem	No	2 papers
369	The hot spots conjecture for simply connected planar domains	Yes	–
370	The Lane–Emden and Hénon–Lane–Emden conjectures	Yes	Part of the paper not formalized
371	Stable blowup for the defocusing Schrödinger equation	Yes	Definition holes: needs a human check
372	Global uniqueness in smooth isotropic elasticity	Yes	–
373	Nonattainment of the three-marginal Coulomb Monge problem	Yes	Part of the paper not formalized
374	Sharp one-third stability of Brenier maps	Yes	Definition holes: needs a human check
375	De Giorgi's conjecture in dimension eight	No	–
376	Universal computation in forced Navier–Stokes flows	Yes (6 checks)	Part of the paper not formalized; 9 papers
377	Interior C^1,α regularity for infinity-harmonic functions	No	–

What the numbers do and do not say

The README says about 42% of "top-line results" are formalized, while 242 of 372 families (65%) have a Lean scope note. The repository does not explain the difference, so we report both figures rather than pick one.

According to the README, the papers came from an unreleased internal OpenAI model. About 4,000 problems were posed, and each result used about three hours of ChatGPT Pro thinking compute on average. Two pieces of work followed a different procedure, and one write-up was human-edited for readability. The formalization catalogue lists its automation method as "agent" and its review status as "unchecked", and the README does not describe peer review. Formalization lowers the risk of a wrong proof sharply. Whether a formal statement says what the paper claims is still a question for mathematicians to settle.

Sources

lean-lang.org, The Lean Language Reference, "Validating a Lean Proof" (accessed 2026-10-13) — lean-lang.org/doc/reference/latest/ValidatingProofs/. The four check levels, the reading of #print axioms, the blue-tick caveat, and the "malicious" category including un-reviewed AI-generated proofs.
lean-lang.org, The Lean Language Reference, "Axioms" (accessed 2026-10-13) — lean-lang.org/doc/reference/latest/Axioms/. sorryAx and native evaluation.
Avigad, de Moura, Kong, Ullrich, Theorem Proving in Lean 4, chapters "Axioms and Computation" and "Tactics" — lean-lang.org/theorem_proving_in_lean4/. The three standard axioms and the "declaration uses 'sorry'" warning.
Lean developers, Comparator README — github.com/leanprover/comparator. Challenge and solution files, the three guarantees, definition holes, nanoda.
OpenAI, openai/math repository at commit 1581d4c (2026-10-12) — github.com/openai/math: README.md, CONTENTS.md, lean/formalization.yaml, lean/docs/, lean/ComparatorChallenges/ (including PeriodicGroup.lean, PeriodicGroup.json and its README).
OpenAI, An infinite finitely presented periodic group, preprint, 23 September 2026 — paper.pdf.

Frequently asked questions

What does "Lean-checked" mean?

It means the Lean kernel accepted a proof of the theorem statement as written in Lean, following only from the definitions, theorems and axioms in the file and its imports. It does not confirm that the Lean statement says the same thing as the English paper; a person has to read the statement and its definitions for that.

Does a sorry in a Lean file mean the proof is wrong?

It means that step is not proved. Lean warns "declaration uses `sorry`" ("declaration uses 'sorry'" before Lean 4.28), and the sorryAx axiom behind it can prove anything, so a theorem that depends on sorry is unproved. The exception is a Comparator challenge file: it states the theorem with sorry on purpose, and the proof lives in a separate solution file.

Which axioms are acceptable in a Lean proof?

Lean's reference manual calls propext, Classical.choice and Quot.sound the standard, benign axioms. If #print axioms also lists sorryAx, the proof is incomplete; a name containing _native means native evaluation was trusted; any other axiom was declared by the author, and the theorem only holds if that axiom is true.

How many of OpenAI's 2026 math results are Lean-checked?

At repository commit 1581d4c (2026-10-12), 242 of the 372 result families had a Lean formalization page and published Comparator checks, while the README says about 42% of top-line results are formalized. All 416 checks allow only the three standard axioms, 80 scope pages say part of the paper is not formalized, and the catalogue lists its review status as "unchecked".

Is a Lean-checked AI result accepted mathematics?

Not on its own. A Lean check is strong evidence that the formal statement is true, but mathematicians still need to confirm the statement matches the claim, and Lean's own guide treats un-reviewed AI-generated proofs as possibly misleading, recommending a sandboxed Comparator check with an independent second kernel.

Was this article helpful?