Trace rank and characteristic-zero Kaplansky idempotents for torsion-free groups
Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.
Theorem selected for verification:OAI.TorsionFreeBass.torsion_free_corollary
The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.
theoremtorsion_free_corollary (G : Type*) [Group G] (hG : TorsionFree G) : ((∀ (q : ℕ), 1 ≤ q → ∀ e : Matrix (Fin q) (Fin q) (MonoidAlgebra ℂ G), e ^ 2 = e → matrixTrace e = ((augmentedMatrix e).rank : ℂ)) ∧ traceK0 (G := G) = (Int.castAddHom ℂ).comp augmentationRank ∧ Set.range (traceK0 (G := G)) = Set.range (fun z : ℤ => (z : ℂ))) ∧ (∀ (R : Type*) [CommRing R] [IsDomain R] [CharZero R] (e : MonoidAlgebra R G), e ^ 2 = e → e = 0 ∨ e = 1) := bysorry
A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.
Definitions needed to read it
Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.
noncomputabledefclassCoefficient {G : Type*} [Group G] (g : G) (a : MonoidAlgebra ℂ G) : ℂ := by classical exact a.coeff.sum fun h z => if IsConj h g then z else0
defdirectSum (e f : Idempotent R) : Idempotent R where size := e.size+f.size matrix := Matrix.reindexRingEquiv R finSumFinEquiv (Matrix.fromBlocks e.matrix 00 f.matrix) idem := by rw [←map_mul,Matrix.fromBlocks_multiply] simp only [Matrix.mul_zero,Matrix.zero_mul,add_zero,zero_add,e.idem,f.idem]
Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.
Words of the Lean statement, its names split into words, that also appear in the theorem: rank, torsion, subgroup, characteristic, free, idempotent, zero and group. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: commutative, unital and domain.
Statements in The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture come first because the release lists only that paper for this Lean statement.
Corollary 1.2 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture
Corollary
Let G be any torsion-free discrete group.
(i)
For every q\geq1 and every idempotent e\in M_q(\C G),
Let $G$ be any torsion-free discrete group.
\begin{enumerate}[label=\textup{(\roman*)}]
\item For every $q\geq1$ and every idempotent $e\in M_q(\C G)$,
\[
\tau_{G,q}(e)=\operatorname{rank}_{\C}\bigl(\epsilon_{G,q}(e)\bigr).
\]
Consequently $\tau_{G,*}=\operatorname{rk}_{\epsilon}$, with
$\Z$ viewed as a subgroup of $\C$, and
\[
\tau_{G,*}\bigl(K_0(\C G)\bigr)=\Z.
\]
\item For every commutative unital domain $R$ of characteristic zero,
every $e\in RG$ satisfying $e^2=e$ is either $0$ or $1$.
\end{enumerate}
Other possible paper matches, closest wording first
Theorem 1.1 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture. Words of the Lean statement, its names split into words, that also appear in the theorem: element, order, finite and group. Found in the paper’s title, which its main theorem states: bass, characteristic, idempotent, zero and trace.
Corollary 9.1 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture. Words of the Lean statement, its names split into words, that also appear in the theorem: hattori, stallings, trace and group.
Proposition 7.3 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture. Words of the Lean statement, its names split into words, that also appear in the theorem: complex, image and integer.
Proposition 5.4 of The ℓ¹-Bass Conjecture for Discrete Groups. Words of the Lean statement, its names split into words, that also appear in the theorem: scalar, coefficients, identity, dimensions, zero and trace.
Theorem 2.1 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture. Words of the Lean statement, its names split into words, that also appear in the theorem: image, integer, zero and group.
Proposition 2.2 of The ℓ¹-Bass Conjecture for Discrete Groups. Words of the Lean statement, its names split into words, that also appear in the theorem: subgroup, order, finite, idempotent, trace and group.
How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.
Reported Comparator runs
two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.
For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.
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 (.github/workflows/openai-math-kernel.yml), one j…
AcceptedTheir term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
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.
AcceptedTheir term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.
This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.
Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.
Do family 207’s Lean statements express the advertised result?
These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.
Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.
Finds part of it stated, or a narrower or weaker statementTheir term: “weaker-statement”.
The challenge statements do not imply the headline claim: they state a nontrivially weaker statement. Their record
Their note: Headline is the ℓ¹-Bass conjecture over ℓ¹(G), but bassTraceModules_vanishing_and_support is only about the group algebra MonoidAlgebra ℂ G (Hattori-Stallings trace of every K0 class vanishes off finite-order classes and is supported on them); no ℓ¹(G) appears anywhere (docs: 'proves the complex Bass trace conjecture for every group'; docs title says ℓ¹ but scope does not). The algebraic companion IS stated: torsion_free_corollary gives trace = augmentation rank on K0(ℂ[G]) and ∀ R comm. domain with CharZero, e^2 = e → e = 0 ∨ e = 1 for torsion-free G.
Definitions the group asks readers to compare with the paper: Hand-rolled K0: BassTrace.K0.Group R := FreeAbelianGroup (Idempotent R) ⧸ relations R (relations: e ~ f when a*b = e ∧ b*a = f, plus direct sums) and ModuleK0 of f.g. projective right modules, HattoriStallings into ConjClasses G →₀ ℂ; standard presentations, not Mathlib objects.
Finds part of it stated, or a narrower or weaker statementTheir term: “NARROWER — UNDECLARED”.
The challenge statements state less than the headline, and OpenAI’s Lean note does not say so. Their record
Their note: The ℓ¹(G) version (the family's titular result and the October 5 paper) and the integral Bass trace conjecture for K₀(ℤG) are not stated. Only the ℂ[G] Bass conjecture and the torsion-free consequences are.
OpenAI’s own note on what this Lean statement covers
“For torsion-free $G$, it identifies the trace on $K_0(\mathbb C[G])$ with the integral augmentation rank and proves the characteristic-zero Kaplansky idempotent conjecture: for every commutative unital domain $R$ of characteristic zero, an idempotent in $R[G]$ is $0$ or $1$.”
An AI agent drafted an interpretation of that note, classifying this statement as “states a consequence of a paper’s theorem”. No human review of the draft is recorded.
Supporting material
The complete Lean statement file
312 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.
Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.
Links in the file: 111 to its own declarations, 232 to Mathlib’s documentation. 35 declared names also link to the same declaration in OpenAI’s library. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.
Let $G$ be any discrete group. For every $x\in K_0(\C G)$ and every
infinite-order element $g\in G$,
\[
\HS_G(x)([g]_G)=0.
\]
Equivalently, if $\con_{\mathrm{fin}}(G)$ denotes the conjugacy classes of
finite-order elements, then
\[
\HS_G\bigl(K_0(\C G)\bigr)
\subseteq\bigoplus_{C\in\con_{\mathrm{fin}}(G)}\C C.
\]
Corollary
Let G be any torsion-free discrete group.
(i)
For every q\geq1 and every idempotent e\in M_q(\C G),
Let $G$ be any torsion-free discrete group.
\begin{enumerate}[label=\textup{(\roman*)}]
\item For every $q\geq1$ and every idempotent $e\in M_q(\C G)$,
\[
\tau_{G,q}(e)=\operatorname{rank}_{\C}\bigl(\epsilon_{G,q}(e)\bigr).
\]
Consequently $\tau_{G,*}=\operatorname{rk}_{\epsilon}$, with
$\Z$ viewed as a subgroup of $\C$, and
\[
\tau_{G,*}\bigl(K_0(\C G)\bigr)=\Z.
\]
\item For every commutative unital domain $R$ of characteristic zero,
every $e\in RG$ satisfying $e^2=e$ is either $0$ or $1$.
\end{enumerate}
Consequently \tau_{G,*}=\operatorname{rk}_{\epsilon}, with \Z viewed as a subgroup of \C, and
\tau_{G,*}\bigl(K_0(\C G)\bigr)=\Z.
(ii)
For every commutative unital domain R of characteristic zero, every e\in RG satisfying e^2=e is either 0 or 1.
The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture
TeX label cor:torsion-free, build/sections/01-introduction.tex, line 98
The Lean statement says
theoremtorsion_free_corollary (G : Type*) [Group G] (hG : TorsionFree G) : ((∀ (q : ℕ), 1 ≤ q → ∀ e : Matrix (Fin q) (Fin q) (MonoidAlgebra ℂ G), e ^ 2 = e → matrixTrace e = ((augmentedMatrix e).rank : ℂ)) ∧ traceK0 (G := G) = (Int.castAddHom ℂ).comp augmentationRank ∧ Set.range (traceK0 (G := G)) = Set.range (fun z : ℤ => (z : ℂ))) ∧ (∀ (R : Type*) [CommRing R] [IsDomain R] [CharZero R] (e : MonoidAlgebra R G), e ^ 2 = e → e = 0 ∨ e = 1) := bysorry
A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.
Recorded comparisons with the paper
Atlas records no contributed comparison of this statement with the paper.
Contributed Comparator run reports
Atlas records no contributed report of running Comparator for this statement file.