Failure of rational injectivity for maximal coarse assembly
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Constructs a uniformly discrete bounded-geometry space whose maximal coarse assembly map is not rationally injective. The example is a coarse disjoint union of finite connected graphs of uniformly bounded degree, with an infinite-order kernel class. A companion gives the analogous failure for reduced coarse assembly, disproving the rational coarse Novikov 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.
There is a uniformly discrete bounded-geometry metric space X, which is a coarse disjoint union of finite connected graphs of uniformly bounded degree, and an infinite-order element \alpha\in KX_1(X) such that
\mu_X(\alpha)=0\quad\text{in }K_1(C^*(X)).
Consequently, ordinary coarse assembly for X fails to be injective both integrally and after tensoring its domain and target with \Q.
The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.
There exist finite connected graphs (X_j)_{j\geq1} with a common finite bound on vertex degree, a coarse disjoint union X=\bigsqcup_{j\geq1}X_j, and an infinite-order class \alpha\in\KX_1(X) such that
\mu_X^{\max}(\alpha)=0.
Consequently, \mu_X^{\max}\otimes\Q is not injective.
No Lean statement in the release is paired with this theorem.
The release does not say which paper theorem its catalogue describes. Both statements above are shown whole, the closer match to the description’s wording first. The atlas has not reviewed either choice.
Reported proof verification
One Lean statement in the release; no independent acceptance report is recorded for the version shown here.
We construct a uniformly discrete bounded-geometry space whose maximal coarse assembly map has an infinite-order element in its kernel. The space is a coarse disjoint union of finite connected graphs of uniformly bounded degree, so maximal coarse assembly need not be rationally injective even for such graph unions.
We disprove the coarse Novikov conjecture: ordinary coarse assembly need not be rationally injective for uniformly discrete spaces of bounded geometry. We construct a coarse disjoint union of finite graphs of uniformly bounded degree and an infinite-order class in its degree-one coarse K-homology whose image under ordinary coarse assembly in the K-theory of the reduced, locally compact Roe algebra vanishes.
One Lean statement in this family
Lean is a language for mathematical statements and proofs that a computer can verify. The Lean statement below is shown beside its possible paper counterpart, with the reason they were linked.
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.
There is a uniformly discrete bounded-geometry metric space X, which is a coarse disjoint union of finite connected graphs of uniformly bounded degree, and an infinite-order element \alpha\in KX_1(X) such that
\mu_X(\alpha)=0\quad\text{in }K_1(C^*(X)).
Consequently, ordinary coarse assembly for X fails to be injective both integrally and after tensoring its domain and target with \Q.
The words they share: after, assembly, bounded, coarse, connected, degree, discrete, disjoint, fails, finite, geometry, graphs, infinite, order, ordinary, tensoring, uniformly, union.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
CoarseAssembly.lean, the release lists it as a supporting statement.
theorembounded_geometry_graph_counterexample_unconditional : (∀ j, Finite (FiberVertex j) ∧ (fiberedGraph elementaryMoves chosenHolonomyUnit j).Connected) ∧ (∃ D : ℕ, ∀ j (x : FiberVertex j), Nat.card {y // (fiberedGraph elementaryMoves chosenHolonomyUnit j).Adj x y} ≤ D) ∧ ProperSpace VertexUnion ∧ UniformFiniteBalls VertexUnion ∧ (∀ x y : VertexUnion, x ≠ y → 1 ≤ dist x y) ∧ ∃ α : KX1 VertexUnion, (∀ n : ℤ, n ≠ 0 → n • α ≠ 0) ∧ constructedCoarseAssembly α = 0 ∧ (1 : ℚ) ⊗ₜ[ℤ] α ≠ 0 ∧ ¬ Function.Injective constructedCoarseAssembly ∧ ¬ Function.Injective (constructedCoarseAssembly.toIntLinearMap.lTensor ℚ) := 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.
Atlas has no report of an independent group using Comparator to verify OpenAI’s proof of this Lean statement at the version shown here. Who ran the proof-verification program
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:bounded_geometry_graph_counterexample_unconditional gives finite connected bounded-degree graphs fiberedGraph... j whose coarse union VertexUnion is proper, has uniformly finite balls and separation ≥ 1, and α ∈ KX1 VertexUnion of infinite order with constructedCoarseAssembly α = 0, 1 ⊗ α ≠ 0 and non-injectivity also after ⊗ ℚ, but the target is K₁ of the *reduced* Roe algebra (DiscreteRoe.algebra; the file header says ‘ordinary reduced coarse assembly map’). That is the summary’s companion claim (the rational coarse Novikov counterexample); the headline failure for the *maximal* assembly map is strictly stronger (reduced = quotient ∘ maximal, so ker(max) ⊆ ker(reduced)) and has no statement. Title and summary say ‘maximal’ while docs, lean_scope and the Lean say ‘reduced’, and Lean wins.
Definitions the group asks readers to compare with the paper:The assembly map is built with totalizing fallbacks: separatedIndexFamily is if h : (∀ r s h a, f s (map r s h a) = f r a) then {atScale := f, compatible := h} else {atScale := fun _ => 0,..} and analyticFamilyIndex is if h : relations A ≤ (analyticFamilyIndexFree..).ker then QuotientAddGroup.lift.. else 0, so from the statement alone the map could be the zero map; the solution proves the genuine branches are taken (separatedIndexFamily_atScale, analyticFamilyIndex_eq_lift in OAI/Topology/CoarseAssembly); 6,648-line hand-built stack with no Mathlib counterpart: coarse K-homology KX1 X := (coarsening X).Homology (direct limit over Rips complexes of OddK C₀(P_r X, ℂ), odd Fredholm modules mod CycleRelation degenerate/unitary/directSum/homotopy), K1 A := ker (K₁(A⁺) → K₁ ℂ) via TopologicalK1.Relation (mul/stabilize/homotopy), and vertexUnionMetric = graph metrics on the fibres glued by separatedDist (d(x,o_i) + i + j + 2 + d(o_j,y)); read as standard, not independently re-derived. The statement does not itself say that the fibre metrics are the graph metrics.
“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:failure of rational injectivity for the MAXIMAL coarse assembly map (the headline’s lead claim, the October-5 manuscript); only the reduced (September-23 companion) result is stated
“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.
The coarse Novikov conjecture predicts rational injectivity of the ordinary coarse assembly map for uniformly discrete spaces of bounded geometry. The formalization constructs a counterexample from a coarse disjoint union of finite connected graphs with uniformly bounded degree. Its degree-one coarse $K$-homology contains an infinite-order class whose image under ordinary coarse assembly into the reduced locally compact Roe algebra vanishes. The class remains nonzero after tensoring with $\mathbb Q$, so rational injectivity fails.
AI-drafted comparisons, with no recorded human review
Failure of rational injectivity for ordinary coarse assemblyCoarseAssembly
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: a bounded-geometry coarse union of finite graphs with a rationally nonzero K-homology class killed by coarse assembly, so the coarse Novikov conjecture fails. The maximal-assembly result of the family’s later paper is not part of it.
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.
Failure of rational injectivity for ordinary coarse assemblyCoarseAssembly
Two reports, all at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“REFUSED”
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
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.
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 “Major math journal”. The page says that nothing on it is verified.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The headline claims failure for maximal coarse assembly, but the Lean uses the reduced Roe algebra, which gives the weaker result.
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.
Run Comparator on OpenAI’s proof
Atlas records no independent report that Comparator accepted the proof at the release version shown here.Open the form
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
Identify the theorem the catalogue describes
Family 307The 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 did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
The solution was built and its dependency closure checked; Comparator was not run.
Date
10 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.