A torsion-free group algebra that is not directly finite
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Constructs a finitely presented torsion-free nonsofic group whose group algebra over 𝔽2 is not directly finite, disproving Kaplansky’s conjecture even without torsion. Companion examples give injective nonsurjective cellular automata on all configurations, refuting Gottschalk’s surjunctivity conjecture. Another counterexample is an integral group-ring matrix, invertible over the rational group ring, with Fuglede–Kadison determinant strictly between zero and one, disproving the unrestricted Determinant Conjecture. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement.Read the assessments
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
Four other possible matches are listed below the card, among them Theorem 1.1 in A Torsion-Free Group Algebra That Is Not Directly Finite and Theorem 1.1 in A Counterexample to Kaplansky’s Direct-Finiteness Conjecture in Characteristic Two.
There are a finitely generated discrete group G_D, an integer n\ge1, and A\in\Mat_n(\Z[G_D]) invertible over \Q[G_D] such that
0<\det_{\N(G_D)}(T_A)<1.
The integral in Equation (1.1) is finite and strictly negative. Thus the unrestricted group-ring Determinant Conjecture has a negative resolution.
Four more possible matches
Theorem 1.1in A Torsion-Free Group Algebra That Is Not Directly Finite.
Theorem 1.1in A Counterexample to Kaplansky’s Direct-Finiteness Conjecture in Characteristic Two, 23 September 2026.
Theorem 1.1in A Counterexample to Kaplansky’s Direct-Finiteness Conjecture in Odd Characteristic, 26 September 2026.
We construct a finitely presented torsion-free counterexample to Kaplansky’s direct finiteness conjecture over the field of two elements. The group admits a finite two-dimensional classifying complex.
We disprove Kaplansky’s direct-finiteness conjecture by constructing a finite field K of characteristic two, a finitely presented group G, and finite sums \(a,b\in K[G]\) with \(ab=1\) but \(ba\ne1\). The group G is nonsofic. The same elements define a cellular automaton on KG that is injective but not surjective, disproving Gottschalk’s surjunctivity conjecture.
We disprove the unrestricted group-ring Determinant Conjecture. We construct a finitely generated group G and a square matrix over \(\mathbb Z[G]\) that is invertible over \(\mathbb Q[G]\) and has Fuglede–Kadison determinant strictly between zero and one. The logarithmic integral defining the determinant is finite.
We construct a counterexample to Kaplansky’s direct-finiteness conjecture in odd characteristic. For one specified odd prime p, we obtain a field K of order p4, a finitely generated group G containing torsion, and finite sums \(a,b\in K[G]\) with \(ab=1\) but \(ba\ne1\). The same elements define a cellular automaton on KG that is injective but not surjective.
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
GroupRingDeterminant.lean, the release lists it as a main result.
defMainStatement : Prop := ∃ (G : Type) (_ : Group G) (_ : Group.FG G) (n : ℕ),1 ≤ n ∧ ∃ (A : Matrix (Fin n) (Fin n) (MonoidAlgebra ℤ G)) (T : Hilbert G n →L[ℂ] Hilbert G n), IsUnit (rationalMatrix A) ∧ IsRegularOperator A T ∧ IsUnit T ∧0 < fkDet T ∧ fkDet T < 1⋮theoremmain : MainStatement := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
There exist a finite field K of characteristic two, a finitely presented group G containing an element of odd prime order, and elements a_{\mathrm{out}},b_{\mathrm{out}}\in K[G] such that
KaplanskyDirectFiniteness.lean, the release lists it as a supporting statement.
defMainClaim : Prop := ∃ (K : Type) (_ : Field K) (_ : Fintype K) (_ : CharP K 2), ∃ (G : Type) (_ : Group G) (_ : Group.FG G), ∃ a b : MonoidAlgebra K G, a * b = 1 ∧ b * a ≠ 1⋮theoremmain_theorem : MainClaim := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
There exist a finite field K of characteristic two, a finitely presented group G containing an element of odd prime order, and elements a_{\mathrm{out}},b_{\mathrm{out}}\in K[G] such that
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
Then p is an odd prime. There are a specified field K of order p^4, a specified finitely generated group G containing torsion, and specified finite sums a,b\in K[G] satisfying ab=1 and ba\ne1.
The words they share: min, prime, odd, order, integer, field, finite, group, binom, generated, torsion, finitely.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
OddKaplansky.lean, the release lists it as a main result.
defMainClaim : Prop := sourcePrime.Prime ∧ Odd sourcePrime ∧ ∃ (K : Type) (_ : Field K) (_ : Fintype K) (_ : CharP K sourcePrime), Fintype.card K = sourcePrime^4 ∧ ∃ (G : Type) (_ : Group G) (_ : Group.FG G), (∃ g : G, g ≠ 1 ∧ IsOfFinOrder g) ∧ ∃ a b : MonoidAlgebra K G, a * b = 1 ∧ b * a ≠ 1 ∧ Function.Injective (cellular b) ∧ ¬ Function.Surjective (cellular b)⋮theoremmain_theorem : MainClaim := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
Other mathematical statements in OpenAI’s Lean library
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express part of the advertised result (their term: “partial”).
Their note:Determinant counterexample is stated (GroupRingDeterminant.main: f.g. G, n >= 1, integral matrix A invertible over ℚ[G], bounded left-regular T invertible with 0 < fkDet T < 1, fkDet T = exp(Re tr(CFC.log(T*T))/2)) and a Gottschalk counterexample is stated only for odd characteristic (OddKaplansky: K of order p^4, f.g. G with torsion, ab = 1 ∧ ba ≠ 1, cellular b injective and not surjective). The summary’s headline for Kaplansky is a finitely presented TORSION-FREE NONSOFIC group over F_2: the char-2 statements (KaplanskyDirectFiniteness, KaplanskyFinitelyPresented) give a f.g./f.p. group that has an element of odd prime order, and nonsofic/torsion-free are not stated (docs: ‘The further conclusion that the group is nonsofic is outside these statements’).
Definitions the group asks readers to compare with the paper:@[irreducible] def sourcePrime : ℕ := Nat.minFac ((Nat.factorial sourceM)^2 + 1) with sourceM := Nat.choose 1200 600 in OddKaplansky: the characteristic is a specific astronomically large, non-computable prime; existence of a counterexample is claimed only for this prime (not suspicious in logic, but the statement is for one prescribed p).
“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).
The gap they name:The headline’s lead claim — a TORSION-FREE, nonsofic, finitely presented group with 𝔽2[G] not directly finite — is not stated. The finitely presented Lean example is required to have torsion (∃ g with orderOf g = an odd prime) and lives over an unspecified finite field of characteristic 2. Nonsoficity is declared outside; torsion-freeness and the field 𝔽2 are not mentioned by the scope note, which does not link the October 4 torsion-free manuscript.
“NARROWER — UNLINKED”, in their words: The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
Kaplansky’s direct-finiteness conjecture asserts that $ab=1$ implies $ba=1$ for $a,b\in K[G]$, for every field $K$ and group $G$. The formalized results construct a finite field of characteristic two and a group algebra violating this implication. One statement records the counterexample for a finitely generated group; the more detailed construction gives a finitely presented group with an element of odd prime order.
The detailed construction also gives a precise recipe for choosing the data and proves that the required search terminates. The further conclusion that the group is nonsofic is outside these statements.
A nonsingular integer matrix has absolute determinant at least $1$. The group-ring Determinant Conjecture extends this bound to matrices over $\mathbb Z[G]$ for every discrete group $G$. If $T_A$ is the operator induced by such a matrix $A$ on finite direct sums of $\ell^2(G)$, and $\mu_A$ is the spectral measure of $T_A^*T_A$ with respect to the group trace, the conjecture asserts
$\displaystyle \int_{(0,\infty)}\log t\,d\mu_A(t)\ge0,$
with the zero spectral atom omitted. For an invertible square matrix, this is equivalent to its Fuglede–Kadison determinant being at least $1$.
The formalized result contradicts that bound. It gives a finitely generated group $G$ and an $n\times n$ matrix over $\mathbb Z[G]$, with $n\ge1$, that is invertible over $\mathbb Q[G]$. Its bounded left-regular operator is invertible and has determinant strictly between $0$ and $1$.
The formalization uses the trace of $\log(T^*T)$ to define the determinant for the invertible operator $T$. The paper’s additional spectral-measure integral conclusion is not included.
Kaplansky’s direct-finiteness conjecture asserts that $ab=1$ implies $ba=1$ in every group algebra over a field. Let $p$ be the smallest prime divisor of $\bigl(\binom{1200}{600}!\bigr)^2+1$; this prime is odd. The formalized result constructs a field $K$ of order $p^4$, a finitely generated group $G$ with torsion, and elements $a,b$ violating this implication. The associated cellular automaton on all configurations $K^G$ is injective but not surjective.
The formalization also contains fixed-field transfer results, separate from the statement linked below.
AI-drafted comparisons, with no recorded human review
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: a matrix over Z[G] invertible over Q[G] with Fuglede–Kadison determinant strictly between 0 and 1. The theorem’s statement that the spectral integral is negative is not included, though the note records that for invertible matrices it is equivalent to the determinant bound.
Unreviewed AI draft: states a weaker form of a paper’s theorem. States a characteristic-two counterexample to direct finiteness over a finitely generated group, without the finite presentation and odd-order torsion of the main theorem; KaplanskyFinitelyPresented records those.
Unreviewed AI draft: states a paper’s theorem as the paper does. States the existence assertion of the main theorem: a finite field of characteristic two, a finitely presented group with an element of odd prime order, and a, b with ab = 1, ba ≠ 1. The theorem’s description of the data by a terminating prescription is not part of the statement.
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the odd-characteristic paper: with p the least prime factor of (C(1200, 600)!)² + 1, a field of order p⁴, a finitely generated group with torsion and a, b with ab = 1, ba ≠ 1.
Who ran the proof-verification program?
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
Other people’s accounts of running proof-verification software, with links to their reports.
carlostoledo1891, def_eq unfolds proofs when proof irrelevance fails (issue 44), with a replay of every openai/math challenge, 11 October 2026. Source
KaplanskyDirectFiniteness and KaplanskyFinitelyPresented pass nanoda with a 1 GiB stack (about 7 GB peak, 15 minutes).
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The review reports that Comparator accepted OpenAI’s solution for this challenge, run end to end on Lean 4.34.1 with the default kernel and only the three standard axioms.
Other proofs and exact calculations
These reports examine claims in the papers using exact calculations for finite claims, independently of the release’s Lean proofs. Read each report for the exact claim it covers.
What these papers cite in the release, and what cites them
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
Papers elsewhere in the release that cite this family’s papers
No paper elsewhere in the release cites this family’s papers.
Follow-up work by others
acprk, Remarks on proofs in OpenAI’s mathematics repository, 10 October 2026. Source
Odd-characteristic Kaplansky counterexample made explicit (m reduced from about 1e360 to 6e24).
References outside the release
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Explain a result, compare statements or propose a correction
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a counterexample and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.
grwtsk, [AUDIT.00] Audit the formal trust surface of the OpenAI math release (issue 2), 9 October 2026. Source
Kaplansky family split into four claim layers: target 1 covers finite field, finitely generated group, one-sided inverse; target 2 adds finite presentation and odd-prime torsion; nonsofic and surjunctivity consequences have no matching declaration found.
From github.com/google-deepmind/formal-conjectures, 7 October 2026. Source
Gottschalk surjunctivity left open because only the ring-theoretic statement is formalised in the release.
mo271, Wikipedia/SurjunctiveGroup: gottschalk_surjunctivity_conjecture is false (issue 6919), 7 October 2026. Source
The two Kaplansky counterexample manuscripts give a non-surjunctive (non-sofic) group.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The headline claims a finitely presented torsion-free nonsofic group over the field with two elements; the statements allow any finite field of characteristic two and one needs an element of odd prime order.
Questions awaiting review
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Read the Lean statement against the paper
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
Identify the theorem the catalogue describes
Family 197The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means.Open the form
Address a question raised in an independent assessment
Only a special case is stated, or a co-equal headline claim has no challenge statement.
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Exact calculations for finite claims, cert-machine
Their verdict
“NEEDS DATA”
Claim tested or proved
Cannot be decided from the release: the specific object the argument relies on is not published.
Detail
NOT PUBLISHED; the construction is probabilistic. Section sections/random.tex (input at build/paper.tex line 44); build/sections/topology.tex line 3 (‘The probabilistic argument has produced finite immersed graphs’); build/sections/assembly.tex line 7 (‘sufficiently large’).
Exact calculations for finite claims, cert-machine
Their verdict
“NEEDS DATA”
Claim tested or proved
Cannot be decided from the release: the specific object the argument relies on is not published.
Detail
Not in checkable form. build/sections/01-introduction.tex lines 8-15 (theorem and ‘terminating prescription’); build/sections/04-hypergraph.tex lines 8-20 and 53 (parameters, random slabs, ‘for all sufficiently large h’).
Theorem 1.1 of A Counterexample to Kaplansky’s Direct-Finiteness Conjecture in Odd Characteristic, 26 September 2026
Exact calculations for finite claims, cert-machine
Their verdict
“NEEDS DATA”
Claim tested or proved
Cannot be decided from the release: the specific object the argument relies on is not published.
Detail
Specified but infeasible. Theorem op:main in build/sections/01-introduction.tex lines 14-30; finite data in build/sections/02-finite-data.tex; explicit idempotent eq op:explicit-e in build/sections/03-modular.tex line 191.