OpenAI claim summary for Math-3026

Rational injectivity of reduced coarse assembly

OpenAI's claim

For a uniformly discrete bounded-geometry union of finite graphs, an infinite-order degree-one coarse K-homology class is claimed to have zero ordinary reduced assembly image, contradicting coarse Novikov injectivity. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.

For some uniformly discrete bounded-geometry coarse disjoint union $X$ of finite connected uniformly bounded-degree graphs, OpenAI claims an infinite-order $\alpha\in KX_1(X)$ with \[ \mu_X(\alpha)=0\in K_1(C^*(X)). \] The target is the ordinary reduced Roe algebra and $KX$ is coarse topological $K$-homology. Consequently ordinary coarse assembly is not injective integrally or after rational tensoring. Bounded geometry means each fixed-radius ball has uniformly bounded cardinality.

Outline of the argument

Manuscript 1 (family 307, 2026-09-23): Congruence fibers over growing triangular discs become trivial on their boundary cycles. Short-loop control keeps boundary winding alive through every fixed Rips scale, independently of the index argument. Uniform approximation of constant-fiber projections constructs a Roe-algebra transfer with the exact boundary restriction; the filled base disc then kills the analytic image of that persistent class.

Formal verification

For family 307, the scope page documents the following selections. The ordinary reduced coarse-assembly selection uses a bounded-degree graph union and an infinite-order degree-one kernel class. It does not select the later maximal-completion argument. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: CoarseAssembly.lean. Declarations: OAI.CoarseAssembly.bounded_geometry_graph_counterexample_unconditional.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

• OpenAI, A counterexample to the coarse Novikov conjecture, 2026-09-23; citation key OAI:A-counterexample-to-the-coarse-Novikov-conjecture-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 307: Lean scope.
• Comparator CoarseAssembly.json.
• Comparator CoarseAssembly.lean.
• OpenAI catalogue entry.