cert-machine · audit · OpenAI's math release

OpenAI's 719 manuscripts, checked three ways

On 2026-10-06 OpenAI published 719 mathematical manuscripts produced by an internal model, with Lean formalizations and 416 Comparator challenges. This audit re-runs the kernel check with a second, independent kernel; reads every formal statement against the claim it is supposed to carry; and re-decides, in exact arithmetic with code written here, every claim whose witness is a finite published object. The lanes, words and order were committed before any row was decided.

The release: github.com/openai/math at commit fd4aeeb2 (Apache-2.0; it moved once after our scouting pin adc7f124: 3 manuscripts withdrawn, 14 revised, 11 challenges added). OpenAI calls the collection partial progress, its formal review "unchecked", and says some unformalized results could have issues. Issues and discussions are disabled on the repository; nothing has been sent to OpenAI. A reading is not a certificate, and this page keeps the two apart.

tl;dr

The finding. Kernel lane: 207 of 217 challenges run so far CERTIFIED by Comparator with both Lean's kernel and nanoda (the release had switched nanoda on for 2 of 416); none rejected; 199 not yet decided while the runs continue; the 10 REFUSED are 9 nanoda stack overflows on our runner (re-running with a larger stack), 1 job that hit the runner's time or memory limit. Statement lane: of the 242 families with a Comparator challenge, 127 state their headline; 38 state less and OpenAI's scope note says so; 39 state less because the headline also cites manuscripts the formalization never linked; 23 state less than a linked manuscript claims with nothing saying so; 11 state a different theorem from the headline; 4 carry only a declared supporting result. Finite lane: 42 finite cores CERTIFIED by programs written here (3 of them the whole headline), none refuted; 9 REFUSED (most decided in part, the rest too costly here, each cost named); 15 headline witnesses are asserted but not published in checkable form — among them the Hadwiger, Sidorenko, Ryser and Kaplansky counterexamples.
The mechanism. Three lanes on one pinned commit. K: Comparator, the Lean FRO's judge, re-run on Linux with nanoda — a kernel written in Rust, independently of Lean's — switched on, and a second run that compares the bodies of declared "definition holes", which Comparator checks by type alone. S: every statement read against the family headline, the abstracts and OpenAI's scope note, by two readers wherever the first found a gap. F: a census of all 719 abstracts fixed 66 finite cores before any was decided; each decider is standard-library Python, exact arithmetic, written from the paper before the authors' code was opened, with forged variants that must not certify.
Check it. node tools/pin-openai-math.js · python3 tools/run-openai-math-finite.py --check · node tools/record-openai-math-statements.js · gh workflow run openai-math-kernel.yml -f challenges="…" — the pre-registration is corpus/openai-math/preregistration.json.

kernel lane

207 / 217

Challenges CERTIFIED by two kernels, of those run so far; 416 in all.

statement lane

127 / 242

Families whose Lean states the headline; 23 narrower with nothing saying so.

finite lane

42 / 66

Finite cores certified here; 15 need data the release does not publish; 0 not yet decided.

undecided here

362

Of 719 manuscripts: not linked by any scope note and no finite core. Not doubtful — outside what an exact certifier can decide.

§1 · the kernel lane

Two kernels, every challenge

Comparator builds a challenge and its solution in a sandbox, exports both, checks that each listed theorem has exactly the challenge's statement and uses no axiom beyond propext, Quot.sound and Classical.choice, and replays the proof through Lean's kernel and any external kernel it is given. The release enabled nanoda for 2 challenges; here it is on for all. One job per challenge, on GitHub's Linux runners (Lake and Comparator abort at start on the desk's macOS; the sandbox is Linux-only). A CERTIFIED here says the Lean theorem is proved; whether that theorem is the paper's claim is §3.

verdict	challenge	family	kernels	minutes
REFUSED	DirectedFeedback	102	Lean	35
REFUSED	ErdosReciprocal	159	—	—
REFUSED	GroupRingDeterminant	197	Lean	14
REFUSED	KaplanskyDirectFiniteness	197	Lean	15
REFUSED	KaplanskyFinitelyPresented	197	Lean	15
REFUSED	MinUncut	102	Lean	22
REFUSED	OptimalMaxCut	102	Lean	23
REFUSED	SquareDifference	182	Lean	13
REFUSED	UniqueGamesTheorem	102	Lean	28
REFUSED	VertexCover	102	Lean	18
CERTIFIED	AbhyankarSathaye	049	Lean + nanoda	1
CERTIFIED	AffineBernstein	353	Lean + nanoda	21
CERTIFIED	ArnoldCounterexample	347	Lean + nanoda	23
CERTIFIED	AsymptoticallyMinimalLittlewood	076	Lean + nanoda	7
CERTIFIED	AuslanderReiten	199	Lean + nanoda	48
CERTIFIED	BackwardIntertwiners	293	Lean + nanoda	6
CERTIFIED	BalancedRyser	162	Lean + nanoda	26
CERTIFIED	BallPacking	343	Lean + nanoda	58
CERTIFIED	BallPackingNecessity	343	Lean + nanoda	18
CERTIFIED	BarnetteHamiltonian	180	Lean + nanoda	5
CERTIFIED	BinaryEditLower	099	Lean + nanoda	4
CERTIFIED	BipartiteCrossing	165	Lean + nanoda	5
CERTIFIED	BooneHigman	250	Lean + nanoda	5
CERTIFIED	BorsukNine	156	Lean + nanoda	16
CERTIFIED	BoundedTreewidthL1	089	Lean + nanoda	6
CERTIFIED	Brenier	374	Lean + nanoda	9
CERTIFIED	Brennan	072	Lean + nanoda	9
CERTIFIED	BrennanSharp	072	Lean + nanoda	8
CERTIFIED	C0Absorption	324	Lean + nanoda	5
CERTIFIED	C1EntropyCounterexample	151	Lean + nanoda	8
CERTIFIED	CartierChartCompactnessSupport	066	Lean + nanoda	3
CERTIFIED	CharacterVarietiesAllSeamsSupport	027	Lean + nanoda	50
CERTIFIED	CirculantHadamard	179	Lean + nanoda	4
CERTIFIED	ClassicalON	215	Lean + nanoda	15
CERTIFIED	CliqueFreeLog	184	Lean + nanoda	4
CERTIFIED	CommutingDerivations	049	Lean + nanoda	2
CERTIFIED	CompactBanach	098	Lean + nanoda	4
CERTIFIED	CompleteCrouzeix	325	Lean + nanoda	8
CERTIFIED	ComplexCancellation	047	Lean + nanoda	7
CERTIFIED	ContinuousCircleWeight	293	Lean + nanoda	8
CERTIFIED	ContinuumTransition	228	Lean + nanoda	18
CERTIFIED	Cotype	326	Lean + nanoda	9
CERTIFIED	CoulombCounterexample	373	Lean + nanoda	5
CERTIFIED	CriticalPercolation	213	Lean + nanoda	21
CERTIFIED	CriticalZ3	213	Lean + nanoda	4
CERTIFIED	CycleDecomposition	181	Lean + nanoda	5
CERTIFIED	DefocusingNLS	371	Lean + nanoda	70
CERTIFIED	DegreeRigidity	241	Lean + nanoda	33
CERTIFIED	DilutedSpin	221	Lean + nanoda	24
CERTIFIED	DimensionTenChannel	272	Lean + nanoda	37
CERTIFIED	DirectCrouzeix	325	Lean + nanoda	7
CERTIFIED	DirichletSevenEighths	003	Lean + nanoda	110
CERTIFIED	DiscreteLipschitzFree	330	Lean + nanoda	3
CERTIFIED	DiskMaximal	085	Lean + nanoda	8
CERTIFIED	Dixmier	251	Lean + nanoda	2
CERTIFIED	DixmierAllDiscrete	251	Lean + nanoda	3
CERTIFIED	DoublingHilbert	098	Lean + nanoda	4
CERTIFIED	DyadicAvoidance	084	Lean + nanoda	3
CERTIFIED	EditDistance	099	Lean + nanoda	7
CERTIFIED	EilenbergGanea	249	Lean + nanoda	62
CERTIFIED	ElementaryPositivity	169	Lean + nanoda	34
CERTIFIED	EuclideanFiveColor	158	Lean + nanoda	8
CERTIFIED	EuclideanRamsey	172	Lean + nanoda	6
CERTIFIED	EuclideanRamseyCircle	172	Lean + nanoda	7
CERTIFIED	EuclideanRamseyNine	172	Lean + nanoda	3
CERTIFIED	EuclideanRamseyQuadratic	172	Lean + nanoda	6
CERTIFIED	EuclideanRamseySpherical	172	Lean + nanoda	5
CERTIFIED	EuclideanRamseyTransitive	172	Lean + nanoda	5
CERTIFIED	EvenBarker	179	Lean + nanoda	5
CERTIFIED	ExactFourier	130	Lean + nanoda	7
CERTIFIED	FactorGeneration	296	Lean + nanoda	48
CERTIFIED	FalconerAllDimensions	073	Lean + nanoda	83
CERTIFIED	FiniteCongruenceGraph	206	Lean + nanoda	0
CERTIFIED	FiniteFactor	293	Lean + nanoda	12
CERTIFIED	FinitisticAsymmetry	198	Lean + nanoda	33
CERTIFIED	FixedClauseThreshold	235	Lean + nanoda	3
CERTIFIED	FormulaHitting	116	Lean + nanoda	1
CERTIFIED	FoulkesHowe	210	Lean + nanoda	5
CERTIFIED	FourierLLogL	075	Lean + nanoda	15
CERTIFIED	FourRowPermanent	238	Lean + nanoda	1
CERTIFIED	GaussianMoat	028	Lean + nanoda	8
CERTIFIED	GaussianPropeller	096	Lean + nanoda	11
CERTIFIED	GeneralizedStarHeight	134	Lean + nanoda	4
CERTIFIED	GeneralMahler	087	Lean + nanoda	103
CERTIFIED	GotsmanLinial	127	Lean + nanoda	1
CERTIFIED	GrahamSpherical	172	Lean + nanoda	1
CERTIFIED	HadamardCubeFiber	266	Lean + nanoda	1
CERTIFIED	HadwigerCounterexample	157	Lean + nanoda	12
CERTIFIED	HalvingLines	183	Lean + nanoda	9
CERTIFIED	HarmonicArtin	254	Lean + nanoda	30
CERTIFIED	HarmonicGrowth	361	Lean + nanoda	21
CERTIFIED	HeilbronnTriangle	191	Lean + nanoda	12
CERTIFIED	Heisenberg	271	Lean + nanoda	23
CERTIFIED	HenonEmden	370	Lean + nanoda	13
CERTIFIED	HoneycombBridgeFiniteness	237	Lean + nanoda	5
CERTIFIED	HoneycombBridgeMassSupport	237	Lean + nanoda	45
CERTIFIED	HoneycombFreeEnergy	237	Lean + nanoda	1
CERTIFIED	HotSpots	369	Lean + nanoda	11
CERTIFIED	HyperinvariantSubspaces	293	Lean + nanoda	11
CERTIFIED	InfiniteMatroid	185	Lean + nanoda	3
CERTIFIED	InfiniteMatroidCorollaries	185	Lean + nanoda	3
CERTIFIED	InterpolatedFactors	287	Lean + nanoda	26
CERTIFIED	IsometricImmersion	334	Lean + nanoda	10
CERTIFIED	Jacobsthal	021	Lean + nanoda	48
CERTIFIED	JacobsthalImproved	021	Lean + nanoda	55
CERTIFIED	JointDickman	012	Lean + nanoda	45
CERTIFIED	KadisonRingrose	295	Lean + nanoda	22
CERTIFIED	KaplanskyQuasitrace	294	Lean + nanoda	13
CERTIFIED	Kervaire	256	Lean + nanoda	8
CERTIFIED	KServer	110	Lean + nanoda	6
CERTIFIED	LipschitzEquivalence	324	Lean + nanoda	10
CERTIFIED	ListHadwiger	157	Lean + nanoda	6
CERTIFIED	LittleFinitistic	198	Lean + nanoda	31
CERTIFIED	LittlewoodFiniteFlatness	076	Lean + nanoda	4
CERTIFIED	LogBrunnMinkowski	091	Lean + nanoda	9
CERTIFIED	LogspaceEquality	103	Lean + nanoda	8
CERTIFIED	MahlerConjecture	087	Lean + nanoda	8
CERTIFIED	MassAction	149	Lean + nanoda	3
CERTIFIED	MatchingAffineLift	126	Lean + nanoda	7
CERTIFIED	MatchingEntropy	113	Lean + nanoda	2
CERTIFIED	MatchingPSD	126	Lean + nanoda	7
CERTIFIED	MetricEntropyDuality	329	Lean + nanoda	1
CERTIFIED	MetricKMedian	125	Lean + nanoda	19
CERTIFIED	Naimark	297	Lean + nanoda	56
CERTIFIED	NodalLength	350	Lean + nanoda	11
CERTIFIED	OccupiedOverlap	238	Lean + nanoda	8
CERTIFIED	OddKaplansky	197	Lean + nanoda	10
CERTIFIED	OneTapeSpace	137	Lean + nanoda	4
CERTIFIED	OrdinaryElliott	007	Lean + nanoda	29
CERTIFIED	OrdinaryTwoPointCorrelations	007	Lean + nanoda	42
CERTIFIED	OstmannComplete	013	Lean + nanoda	59
CERTIFIED	OstmannPrimes	013	Lean + nanoda	172
CERTIFIED	PeriodicGroup	247	Lean + nanoda	12
CERTIFIED	PeriodicTilingThree	155	Lean + nanoda	6
CERTIFIED	PermanentCubic	108	Lean + nanoda	14
CERTIFIED	PettyProjectionVolume	088	Lean + nanoda	9
CERTIFIED	PiExponent	017	Lean + nanoda	45
CERTIFIED	PinnedDistances	167	Lean + nanoda	9
CERTIFIED	PlanarAndersonSpectrum	261	Lean + nanoda	2
CERTIFIED	PlanarFalconer	073	Lean + nanoda	30
CERTIFIED	PlanarL1	089	Lean + nanoda	7
CERTIFIED	PlanarUnitDistances	167	Lean + nanoda	8
CERTIFIED	PlaneColoring	158	Lean + nanoda	1
CERTIFIED	PowerFreeValues	020	Lean + nanoda	14
CERTIFIED	PrimeGaps	026	Lean + nanoda	12
CERTIFIED	ProjectionCounterexample	088	Lean + nanoda	2
CERTIFIED	ProjectionVolume	088	Lean + nanoda	4
CERTIFIED	QuadricBundles	050	Lean + nanoda	10
CERTIFIED	QuantitativeVanDerWaerden	160	Lean + nanoda	4
CERTIFIED	QuasiRiemannHypothesis	003	Lean + nanoda	123
CERTIFIED	QuinticLienard	143	Lean + nanoda	18
CERTIFIED	RadialDensityInterval	228	Lean + nanoda	14
CERTIFIED	RadialTransition	228	Lean + nanoda	10
CERTIFIED	RamseyFive	170	Lean + nanoda	31
CERTIFIED	RealL1Renorming	330	Lean + nanoda	2
CERTIFIED	ReflexiveFixedPoints	328	Lean + nanoda	4
CERTIFIED	RegularParity	274	Lean + nanoda	4
CERTIFIED	RieszQuantitative	081	Lean + nanoda	35
CERTIFIED	Rokhlin	145	Lean + nanoda	11
CERTIFIED	RyserCovering	162	Lean + nanoda	4
CERTIFIED	RyserOddExtensions	162	Lean + nanoda	3
CERTIFIED	SATComputability	235	Lean + nanoda	33
CERTIFIED	SATVariance	235	Lean + nanoda	5
CERTIFIED	SecondKahnKalai	176	Lean + nanoda	1
CERTIFIED	SelfSimilar	148	Lean + nanoda	8
CERTIFIED	SensitivitySeparation	132	Lean + nanoda	2
CERTIFIED	SeparableQuotientNegative	323	Lean + nanoda	8
CERTIFIED	SeymourSecondNeighborhood	173	Lean + nanoda	1
CERTIFIED	SharpLogRamsey	170	Lean + nanoda	23
CERTIFIED	SharpThreshold	186	Lean + nanoda	3
CERTIFIED	ShortEgyptianFractions	025	Lean + nanoda	7
CERTIFIED	SidorenkoCounterexample	161	Lean + nanoda	14
CERTIFIED	SiegelZeros	003	Lean + nanoda	17
CERTIFIED	SignedFiniteBand	085	Lean + nanoda	9
CERTIFIED	SimpleAmenable	253	Lean + nanoda	35
CERTIFIED	SimpleOvergroups	250	Lean + nanoda	16
CERTIFIED	SingleFold	242	Lean + nanoda	5
CERTIFIED	SingleLatticeCovering	092	Lean + nanoda	13
CERTIFIED	SmoothInitialForm	108	Lean + nanoda	6
CERTIFIED	SnakyConditional	187	Lean + nanoda	37
CERTIFIED	SnakyTwentyOne	187	Lean + nanoda	36
CERTIFIED	SpinAngle	238	Lean + nanoda	5
CERTIFIED	SquareRootDegree	192	Lean + nanoda	4
CERTIFIED	StableCoordinateFour	049	Lean + nanoda	4
CERTIFIED	StandardMapEntropy	146	Lean + nanoda	23
CERTIFIED	SteinitzBergstrom	097	Lean + nanoda	8
CERTIFIED	StrictMeans	072	Lean + nanoda	10
CERTIFIED	StrongKadisonKastler	289	Lean + nanoda	208
CERTIFIED	StrongThinTree	174	Lean + nanoda	10
CERTIFIED	SubpolynomialLp	094	Lean + nanoda	9
CERTIFIED	Superstring	128	Lean + nanoda	6
CERTIFIED	SurfaceConeCandidateSupport	195	Lean + nanoda	8
CERTIFIED	SurfaceImmersion	333	Lean + nanoda	79
CERTIFIED	SymmetricDomains	058	Lean + nanoda	24
CERTIFIED	SymmetricMahlerEquality	087	Lean + nanoda	11
CERTIFIED	SymmetricPolar	087	Lean + nanoda	10
CERTIFIED	Tachikawa	199	Lean + nanoda	14
CERTIFIED	TalagrandDiscreteConvexity	175	Lean + nanoda	1
CERTIFIED	TalagrandExpectationThreshold	175	Lean + nanoda	1
CERTIFIED	ThorpWeightedCompatibility	238	Lean + nanoda	3
CERTIFIED	TingleySphereIsometry	322	Lean + nanoda	2
CERTIFIED	TorsionFreeHyperbolic	252	Lean + nanoda	5
CERTIFIED	TorsionFreeZeroDivisors	196	Lean + nanoda	8
CERTIFIED	TraceIdealTransportSupport	301	Lean + nanoda	3
CERTIFIED	TreeEdit	099	Lean + nanoda	4
CERTIFIED	TriangleRemoval	188	Lean + nanoda	12
CERTIFIED	TriangularCovering	100	Lean + nanoda	3
CERTIFIED	TriangularHilbert	082	Lean + nanoda	13
CERTIFIED	TruffetCounterexample	104	Lean + nanoda	1
CERTIFIED	TwoWayComplementation	129	Lean + nanoda	2
CERTIFIED	TwoWayDeterminization	129	Lean + nanoda	3
CERTIFIED	UniformCommutator	288	Lean + nanoda	140
CERTIFIED	UniformFourier	130	Lean + nanoda	5
CERTIFIED	UniformSparsestCut	117	Lean + nanoda	8
CERTIFIED	UniversalFInfinity	250	Lean + nanoda	7
CERTIFIED	VlasovMaxwell	362	Lean + nanoda	23
CERTIFIED	YauCounterexample	350	Lean + nanoda	28

The trust base, as the pre-registration states it: the two kernels, lean4export, Comparator's comparison code, landrun's Landlock sandbox on the runner (recorded per job; Comparator calls landrun with --best-effort, so the job records the kernel's LSM list), the Mathlib cache fetched by lake exe cache get, and GitHub's runners. Comparator's README also asks for systemd-run with AF_UNIX restricted; GitHub's runners have no user systemd session, so that guard is NOT applied, and the page says so.

§2 · definition holes

Where Comparator checks only a type

10 challenges list definitions in definition_names. For those, Comparator compares the definition's name, universe levels, type and safety — never its body (Comparator/Compare.lean, definitionHoleMatches, at the pinned revision) — and its own README says such solutions "must always be checked with an additional (potentially human) verifier". Of the 65 holes these files declare, 63 are displayed with a full body and 2 are left sorried: a reader of the challenge sees 63 definitions the check does not compare. Lane K runs each of these configs twice: as published, and with the holes emptied, which compares every body constant by constant.

challenge	holes (displayed)	bodies, decided
Brenier	12 (12)	SAME BODIES
DefocusingNLS	3 (2)	BODIES DIFFER OAI.DefocusingNLS.sobolevOddPower
ElementaryPositivity	1 (0)	SAME BODIES
EuclideanFiveColor	1 (1)	SAME BODIES
KServer	9 (9)	SAME BODIES
LogspaceEquality	20 (20)	SAME BODIES
Naimark	7 (7)	SAME BODIES
OccupiedOverlap	5 (5)	BODIES DIFFER OAI.RowColumn.OccupiedOverlapEndpoint
Rokhlin	4 (4)	SAME BODIES
SpinAngle	3 (3)	BODIES DIFFER OAI.SpinAngle.missingInRow

Where the strict run names a constant whose bodies differ (OAI.DefocusingNLS.sobolevOddPower, OAI.RowColumn.OccupiedOverlapEndpoint, OAI.SpinAngle.missingInRow), the source text of that definition in the challenge file and in the solution reads the same, line for line, on our reading; the kernel terms differ through elaboration — auxiliary constants, binders, instances — which is presumably why the definitions were declared holes. Comparator alone therefore checks those theorems against a type, and whether the two elaborations mean the same thing is a reading this audit has not yet finished. It is not a finding that anything is wrong.

§3 · the statement lane

What the Lean states, family by family

OpenAI writes one headline per family; a family can hold several manuscripts and several challenges, and its scope note names the manuscripts the formalization covers. Each family's challenges were read against that headline, clause by clause. The words, least to most severe: MATCHES · NARROWER — DECLARED · NARROWER — UNLINKED · NARROWER — UNDECLARED · DIFFERENT, and SUPPORT-ONLY when every challenge is a declared supporting result. Where two readers disagreed, the less severe word is recorded (40 disagreements, 39 of them only because the first readers did not yet have the UNLINKED word).

word	families
MATCHES	127
NARROWER — DECLARED	38
NARROWER — UNLINKED	39
NARROWER — UNDECLARED	23
DIFFERENT	11
SUPPORT-ONLY	4

The 34 families below are the DIFFERENT and NARROWER — UNDECLARED words; each line names what the headline claims and no challenge states. Every such row quotes both texts, with file and line, in certs/openai-math-statements.json.

word	family	claimed, not stated in Lean
DIFFERENT	033 · Iitaka subadditivity, variation, and logarithmic additivity	Proves Campana's orbifold Iitaka subadditivity conjecture for smooth Fujiki-class-\mathcal C manifolds with rational simple-normal-crossing boundaries. · For projective fibrations f:U\to V of smooth complex quasi-projective varieties with connected fibers,…
DIFFERENT	058 · Semialgebraic universal covers and bounded domains	Proves the Kollár–Pardon conjecture: the semialgebraic universal covers of connected normal projective complex varieties are exactly products D\times\mathbb C^m\times F, with D bounded symmetric and F simply connected, normal, and projective. · A universal…
DIFFERENT	194 · Lech’s multiplicity conjecture	Proves e(R)\le e(S) for every flat local homomorphism of nonzero Noetherian local rings, where e is Hilbert–Samuel multiplicity. · This resolves Lech's conjecture in every dimension and characteristic.
DIFFERENT	206 · Finite lattice representation and undecidability	Some finite lattices are not congruence lattices of any finite algebra, answering the finite lattice representation problem negatively. · Moreover, no algorithm decides whether a finite lattice has such a representation, or whether it is a full subgroup…
DIFFERENT	218 · Conformal universality for weakly interacting and random-bond Ising…	Weak finite-range square-symmetric even multispin perturbations of the square-lattice Ising model preserve critical bulk spin and energy limits · weak square-symmetric contour interactions also yield chordal SLE3 interface limits. · With sufficiently weak…
DIFFERENT	237 · The three-quarter exponent for honeycomb self-avoiding walk	Proves the diameter form of Nienhuis's predicted three-quarter exponent: a uniformly chosen n-step self-avoiding walk on the honeycomb lattice has diameter n^{3/4+o(1)}. · Its local mass and covering numbers have exponent 4/3. · These estimates hold at every…
DIFFERENT	260 · Spacetime Penrose inequalities: enclosing area, charge, rotation,…	Proves the sharp enclosing-area spacetime Penrose inequality for smooth one-ended asymptotically flat initial data in every spatial dimension n ≥ 3, under dominant energy, weak future trapping, positive enclosing area, and the stated decay assumptions. · It…
DIFFERENT	281 · QAOA attains the SK optimum in the thermodynamic-first limit	Proves that QAOA approaches the ground-state energy of the Gaussian zero-field Sherrington–Kirkpatrick model when system size tends to infinity before circuit depth. · For every accuracy, finite depth and deterministic angles independent of size and disorder…
DIFFERENT	290 · Relative bicentralizers and modular spectral recovery	Proves Connes' bicentralizer conjecture for every type III1 factor with separable predual and every faithful normal state. · More generally, for every inclusion N\subset M of von Neumann algebras with separable preduals admitting a faithful normal…
DIFFERENT	291 · Cuntz comparison, nuclear dimension, and equivariant Jiang–Su…	Proves equivariant Jiang–Su stability for every countable discrete amenable group action on a simple separable unital infinite-dimensional nuclear stably finite Jiang–Su-stable C∗-algebra, resolving this case of Szabó's conjecture without restrictions on…
DIFFERENT	356 · Gigli’s characterization of Alexandrov curvature	Proves Gigli's conjecture: in every integer dimension n ≥ 2, Alexandrov curvature at least κ is characterized by the full-support \mathop{\mathrm{RCD}}\nolimits ((n-1)\kappa,n) condition with reference measure \mathcal H^n and distributional sectional…
NARROWER — UNDECLARED	047 · Zariski cancellation and affine fibrations over the complex numbers	It also disproves the Dolgachev–Weisfeiler affine-fibration conjecture: smooth surjections X\to\mathbb A^1 and \mathbb A^5\to\mathbb A^2 have every residue-field fiber isomorphic to affine three-space but are not Zariski-locally trivial.
NARROWER — UNDECLARED	072 · Brennan's conjecture and the integral-means spectrum	The sharp universal integral-means identity is B_{\mathcal S}(t)=\|t\|-1 for t ≤ −2.
NARROWER — UNDECLARED	082 · Annular variation and dyadic absolute bounds for the triangular…	Proves maximal and annular r-variation bounds, for every r > 2, from complex L^3(\mathbb R^2)\times L^3(\mathbb R^2) to L^{3/2}(\mathbb R^2). · and gives almost-everywhere and norm convergence
NARROWER — UNDECLARED	089 · Bounded-distortion L1 embeddings of planar and bounded-treewidth…	The corresponding multicommodity flow–cut gaps are uniformly bounded.
NARROWER — UNDECLARED	091 · Logarithmic and Lp Brunn–Minkowski inequalities and the B-conjecture	and the scalar-dilation B-conjecture for all even log-concave Radon measures. · For Lebesgue volume it also proves the additive Lp Brunn–Minkowski inequality for full-dimensional origin-symmetric convex bodies throughout 0\lt p\lt 1.
NARROWER — UNDECLARED	097 · The Euclidean Steinitz–Bergström bound	A matching lower bound gives the optimal order S_2(d)=\Theta(\sqrt d).
NARROWER — UNDECLARED	104 · Quasipolynomial algorithms for mean-payoff, stochastic and parity…	Gives deterministic algorithms using 2^{O((\log(L+2))^2)} bit operations, for complete binary input length L, for ordinary mean-payoff games · and two separate extensions · They compute exact values and optimal positional strategies in ordinary games · the…
NARROWER — UNDECLARED	107 · Matrix multiplication with exponent at most 9/4	In characteristic zero, some inner dimension na with a > 0.465 permits n^{2+o(1)} rectangular multiplication. · Further square bounds give ω < 2.258 outside finitely many positive characteristics
NARROWER — UNDECLARED	114 · Approximate counting of common integer polymatroid bases	Gives a fully polynomial randomized approximation scheme for counting common integer bases of two integral polymatroids of equal total rank, supplied by exact rank-value oracles. · Capacities are binary-encoded, each integer vector counts once, and oracle…
NARROWER — UNDECLARED	132 · A superquadratic separation of sensitivity and block sensitivity	Constructs total Boolean functions with block sensitivity \mathop{\mathrm{bs}}\nolimits (f)\ge s(f)^\alpha for a fixed α > 2
NARROWER — UNDECLARED	162 · Counterexamples to Ryser’s covering conjecture	A separate construction over extension fields also disproves Gyárfás's monochromatic tree-cover conjecture.
NARROWER — UNDECLARED	172 · Classification of finite Euclidean Ramsey configurations	It also disproves the Leader–Russell–Walters conjecture that every such configuration is a subset of a finite transitive set.
NARROWER — UNDECLARED	180 · Barnette’s Hamiltonian-cycle conjecture	Equivalently, every three-edge path in a finite simple cubic 3-vertex-connected bipartite Pfaffian graph lies in a Hamiltonian cycle.
NARROWER — UNDECLARED	183 · Power savings for planar halving lines and k-sets	More generally, an n-point set with no three collinear has O(n(k+1)^{1/3-\varepsilon_0}) strictly separable k-subsets for 1\le k\le n/2, with an absolute \varepsilon_0\gt 0.
NARROWER — UNDECLARED	207 · The ℓ¹-Bass conjecture for all discrete groups	Proves the ℓ1-Bass conjecture for every discrete group: Hattori–Stallings traces of idempotent matrices over \ell^1(G) are supported on finitely many finite-order conjugacy classes. · The algebraic companion proves the integral Bass trace conjecture
NARROWER — UNDECLARED	230 · Exact Hausdorff gauges for SLE	Resolves Schramm’s Hausdorff-measure question for chordal SLEκ, 0\lt \kappa\lt 8. · finite measure to every trace segment \gamma([s,t]) · and finite expected measure to the trace in every bounded disk.
NARROWER — UNDECLARED	261 · Localization and delocalization in the Anderson model	Resolves the predicted spectral contrast for the lattice Anderson model with independent uniform site potentials. · In dimension two, every positive disorder strength gives almost surely pure-point spectrum. · In every fixed dimension d ≥ 3, sufficiently…
NARROWER — UNDECLARED	273 · The entropy photon-number inequality	and product thermal inputs attain equality even when their entropies differ.
NARROWER — UNDECLARED	274 · Parity is not in QAC0	Xu–Li's reductions give the same bounded-error obstruction for strict majority.
NARROWER — UNDECLARED	299 · The Kirchberg–Rørdam character criterion and infinite tensor-power…	Also, the infinite minimal tensor power of every such algebra without characters is Jiang–Su stable, answering the Dadarlat–Toms question.
NARROWER — UNDECLARED	303 · Weak pure infiniteness and Cuntz-algebra absorption	Consequently, every separable nuclear algebra with this property absorbs \mathcal O_\infty, without unitality or simplicity assumptions.
NARROWER — UNDECLARED	326 · The cotype–cotype conjecture under the approximation property	Equivalently, these cotype assumptions force nontrivial Rademacher type.
NARROWER — UNDECLARED	350 · Yau’s nodal bounds: surfaces and higher dimensions	completing Yau's conjecture there · In dimension five, nodal measure can grow faster than \lambda^{1/2+\varepsilon_0} for some fixed \varepsilon_0\gt 0, ruling out even arbitrarily small power losses.

§4 · the finite lane

The finite objects, decided here

A census of all 719 abstracts, by three readers on disjoint slices, named 66 finite cores over 65 manuscripts before any was decided: 47 published and checkable, 4 published but expensive, 15 asserted but not published in checkable form. Each decider reads the release's own bytes and records their sha256; "whole headline" means the finite object is the entire claim, otherwise the analytic argument around the component is not decided here.

verdict	row	manuscript	what is decided
CERTIFIED	F-009	Catalan's constant is irrational	a finite component: the three finite components of the proof and their comparison, not the headline. (1) the real-place certificate — for the published trial sequences, the right side of eq:energy-dual is <= -2.290939875 (kappa=2) and…
CERTIFIED	F-045	Squarefree values of quartics and power-free values of polynomials	a finite component: the exact parameter certificate of Proposition prop:parameter-certificate (all 3,989 cells for d = 4..8, Table tab:parameter-certificate, the 150 endpoint derivative inequalities), the printed exponent margins, and the…
CERTIFIED	F-103	An explicit failure of complex affine-space cancellation	a finite component: the cylinder isomorphism A[w] = C^[5] (Proposition prop:stabilization), by the paper's printed maps with inverses; NOT A not = C^[4], which carries the counterexample
CERTIFIED	F-105	A stable coordinate that is not a coordinate in four variables	a finite component: f is a one-stable coordinate (an explicit automorphism of C[x1..x4,w] with exhibited inverse sends f to x1), deg f = 5, and every fibre f = lambda is C^[3]; NOT that f is not a coordinate in four variables, which…
CERTIFIED	F-106	An explicit noncoordinate polynomial with affine three-space zero fibre	the whole headline: R/(F) = C^[3] by the paper's printed mutually inverse maps, and grad F vanishes at a point, so F is not a coordinate
CERTIFIED	F-125	Ambiently homeomorphic isolated hypersurfaces of multiplicities two and three	a finite component: Lemma seed:product (the integer relation with E > 0 and both products 1), by the shipped witness and by the printed F_1009 rank certificate, plus the chain arithmetic; not the spectra, the lattice/topology, or the…
CERTIFIED	F-135	The Campana–Peternell conjecture in dimension six	a finite component: Lemma lem:finite-ratio (from the matrices A, C_1, N defined in Section 4, N(xi_i eta_j) = 0 with xi_0 = eta_0 = 1 forces 32 - 20 eta_1 + 3 eta_1^2 = 0); dim_Q K_3 <= 6 by a rank mod 10007 (a certified lower bound on…
CERTIFIED	F-171	The Mahler Conjecture for General Convex Bodies	a finite component: the finite certificates of Appendices 07-08 (the 152-node profile enclosures and every printed node bound and finite sum; the stable-formula identities; the layer rectangles; the chord-error, tail-vector, interpolation…
CERTIFIED	F-174	A product counterexample to the simplex maximum for projection-body volume	the whole headline: K = T10 x T10 violates the proposed simplex bound in dimension 20, with the exact ratio printed
CERTIFIED	F-177	An atomic certificate for triangular-lattice universal optimality	a finite component: every inequality of Lemma lem:finite-certificate (the two 20x20 interval blocks and their inverses, the parameter polytope, the jet / curvature / Taylor envelopes, all 659 Bernstein row minima) and the printed rational…
CERTIFIED	F-178	Universal optimality of the triangular lattice	a finite component: Proposition prop:finite-certificate through its three stronger tables (27 power, 30 column, 37310 Bernstein and 10 tail comparisons) on enclosures of the exact quadrature arrays, the same tables on an exact execution…
CERTIFIED	F-179	A sharp Fourier certificate for planar circle packing	a finite component: every finite certificate the proof cites -- Lemma interpolation:finite (the two inverse certificates via W_+-, the exterior block, the 204 residuals, the table norms) and Lemma signs:bernstein (2436 Bernstein…
REFUSED	F-180	Triangular minimality for planar Coulomb renormalized energy	decided in part (pre-registration amendment 5): the two-dimensional sweeps that carry 2g_d(x) >= K and the negative-part bound (the outer primitive grid, ~7.9e6 interval evaluations; the negative-part grid; L1-L4 over ~4.2e5 rectangles;…
CERTIFIED	F-189	The Gaussian propeller bound in every dimension	a finite component: every finite numerical comparison and enclosure of the m >= 5 exclusion (Appendix cert:arithmetic, Tables sc:interval-table, cert:quantiles, elim:small-table, elim:four-table, elim:final-table and the inline bounds),…
REFUSED	F-195	Finite angular cylinder covers below the half-area bound	a finite component: A_min(K) = sqrt 2, the construction's parameters, every polynomial identity of the coverage proof, and the exact total base area at eps = 1/2000 and tau = 1/4000 (strictly below A_min/2, inside the printed remainder…
NEEDS DATA	F-197	Slope-field perturbations of the two-cylinder covering	NOT PUBLISHED as a specific instance; construction in preprints/Slope-field-perturbations-of-the-two-cylinder-covering-September-27-2026/build/sections/threshold.tex and dictionary.tex with non-explicit smallness thresholds.
NEEDS DATA	F-198	Finite triangular approximation of radial sweeps	NOT PUBLISHED as a specific instance; preprints/Finite-triangular-approximation-of-radial-sweeps-September-27-2026/build/beams.tex l.292 ('For every zeta > 0, the tetrahedron K has a finite cylinder cover ...'), coordinates.tex.
CERTIFIED	F-199	A sharp entropy bound and the simplex inequality for isotropic constants	a finite component: the scalar certificate behind Lemmas sc:bounds and tr:scalar-basic — the central piecewise-polynomial certificate on [-6,10] rebuilt from its eleven seed pairs (residuals, joins, anchors, error budgets, all 44 group…
CERTIFIED	F-209	Randomized quasipolynomial-time mean-payoff games	a finite component (the appendix side result, not the main theorem): on the printed two-variable instance the true minimum is exactly 0, while the substitution rule as formalised in the challenge is forced through x2 = h, x1 = h + 1 to…
REFUSED	F-213	Complex Matrix Multiplication Below 2.258 and Rectangular Bounds	finite components only: the three rectangular witnesses (alpha > 0.465, w(0.709) < 2.092, family omega < 2.267) as finite computations; for omega < 2.258 the barrier, both charts (the 18 MB chart verified as the recursion's output), the…
CERTIFIED	F-214	Staggered extraction for exact matrix multiplication over every field	a finite component: the parameter certificate — the five integer arrays, decoded by the printed rules and contracted by the printed finite formulas, give every printed table value and enclosure and 3(8 log 7 - H_0 - C_)/S_ <…
NEEDS DATA	F-232	Additive hardness and unbounded configuration gaps in bin packing	preprints/Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026/build/source/consequences.tex l.9-24 (proof of Theorem thm:unbounded-gap), /build/source/instance.tex l.26-60 (parameters eq:parameters and…
CERTIFIED	F-234	Hellinger contraction with arbitrary Boolean output bias	a finite component: the scalar certificates of the proof — the induction parameters, the 17 profiles' five Bernstein sign checks, the three-coordinate base table, the 21-box pair interval certificate, and every finite comparison and…
NEEDS DATA	F-248	An explicit power saving for the exact discrete Fourier transform	Interface and lemma in build/sections/synthesis.tex lines 18-60 (Lemma syn:local-certificate at lines 39-46), built from the network of build/sections/network.tex (matrix eq. net:C at line 6; Prop. net:finite-interface at line 370;…
CERTIFIED	F-262	Subset Sum in Time O(2^{0.49n})	a finite component: the numerical certificate of Proposition prop:filtering-moments (Appendix app:numerical) - every printed enclosure, error bound and comparison recomputed in directed rational interval arithmetic; the analytic trapezoid…
CERTIFIED	F-287	Arithmetic classification and non-Pisot singularity for Bernoulli convolutions	a finite component: the root location of the degree-31 polynomial (all 31 roots isolated, beta in (1.8392, 1.8393) the only real root, alpha the only other expanding pair, beta not Pisot) and every printed integer of the rational moment…
NEEDS DATA	F-294	A counterexample to Hadwiger's conjecture	NOT PUBLISHED. Theorem thm:main in build/sections/01-introduction.tex lines 20-27; sampling of raw vertices in build/sections/02-geometry.tex lines 258-320; parameter order in build/sections/14-parameters.tex.
NEEDS DATA	F-295	A counterexample to the Colin de Verdière chromatic conjecture	NOT PUBLISHED. Theorem thm:main at build/sections/01-introduction.tex line 42; base graphs Theorem thm:base-graphs at line 147; 'm=2^{1000gN} is the sampled graph order' at lines 315-317.
CERTIFIED	F-297a	The Euclidean plane is not five-colorable	a finite component: Lemma angular-certificate (all seven placed Moser-spindle vertices strictly in the region 0<l<4, P<P'), the eleven unit edges and non-3-colourability, and every number of the paper's rational verification. NOT the…
NEEDS DATA	F-297b	The Euclidean plane is not five-colorable	NOT PUBLISHED. build/sections/introduction.tex lines 31-36 ('an unrestricted lower bound can also be established without first displaying a finite graph witnessing it') and lines 309-313 ('Theorem~\ref{thm:main} and graph compactness ...…
NEEDS DATA	F-300	A counterexample to Sidorenko's conjecture	H: build/sections/complex.tex Table tab:complex at lines 19-56 (Theorem thm:main in build/sections/introduction.tex lines 18-26; Lean ComparatorChallenges/SidorenkoCounterexample.lean def faces). Host: NOT PUBLISHED.…
NEEDS DATA	F-301	Balanced counterexamples to Ryser's conjecture at prime orders	NOT PUBLISHED. Random choices in build/candidates.tex lines 75-140; the random selection procedure in build/selection.tex lines 20-35 ('All subsequent assertions concern sufficiently large q', line 93).
NEEDS DATA	F-302	A counterexample to Ryser's covering conjecture	NOT PUBLISHED. build/selection.tex lines 1-60 (independent random shifts; Lemma sel-domination at line 52).
CERTIFIED	F-336	Snaky in 21 Maker moves	the whole headline (Theorem thm:main, 21 Maker moves on Z^2) and Corollary cor:finite-board, twice: (I) the certificate evaluates to A_727 = {}, h_727 = 21 under the paper's combination rule — sound only with Lemma lem:combination, proved…
CERTIFIED	F-338	Cycle--clique Ramsey numbers	a finite component: the 3099 published deduction traces of Proposition finite:verified exclude all 3099 (pattern, k, t) instances by the paper's stated rules, applied correctly (the rules' soundness and the reduction of R(C_m,K_n) to…
CERTIFIED	F-339	Polynomial removal fails for ordered binary matrices	a finite component: Theorem thm:main at h = 1 and h = 2 (A_1 776 x 776, A_2 3,096 x 3,096), both inequalities decided exactly (N_H(A_h) = 2 m^130 by an exhaustive ordered-copy search; dist_H(A_h) >= eps_h by the sampling argument with…
NEEDS DATA	F-345	A Torsion-Free Group Algebra with Zero Divisors	NOT PUBLISHED. build/sections/factors.tex lines 31-35: 'The construction is probabilistic: it proves that suitable finite matchings exist, without specifying matchings from which a concrete presentation and zero-divisor factors can be…
NEEDS DATA	F-346	A Torsion-Free Group Algebra That Is Not Directly Finite	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');…
NEEDS DATA	F-347	A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic…	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').
NEEDS DATA	F-349	A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Odd…	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.
CERTIFIED	F-351	An explicit counterexample to the Auslander-Reiten conjecture	a finite component: the ten-dimensional algebra C, its trivial extension T and trace, the 179-entry cochain (cocycle and boundary identities, evaluation q^3), the resolution of s over C for every i, and the finite identities of the lift —…
CERTIFIED	F-352	A counterexample to Tachikawa's second conjecture	a finite component: the ten-dimensional algebra C (and its identity with the companion paper's), T and its symmetrizing form, E = T (x) T symmetric nondegenerate, the corner table of B, the exact sequences of Prop a:dual-dimensions, the…
CERTIFIED	F-360	Universal Tensor Squares for Symmetric Groups	a finite component: Proposition prop:finite-check for every eligible n <= 64 (61 of the 61 degrees), with witnesses supplied and certified here (the release records none: NEEDS DATA for its own certificate); the large-degree theory (n >…
REFUSED	F-369	Foulkes' conjecture for the sixth symmetric power	decided in part (pre-registration amendment 5): the base range is decided for b = 6..12 in the ledger run (b = 6..15 in a separate run of this session); b = 13..25 (estimated 8-12 CPU-hours) and the partitions outside the band at b =…
REFUSED	F-409	Microscopic jamming in the negative spherical perceptron	a finite component: stage (I) of the certificate — the two final spectral tests (.2936535023 < lambda(.2936533) < .2936535043, .2936533037 < lambda(.2936535) < .2936533057, hence lambda(a) - a changes sign on (.2936533, .2936535)) by own…
CERTIFIED	F-426	Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase	a finite component: Lemma rcut:lem:scalar-data and Table rcut:tab:scalar-intervals of the appendix route (the independent beta < 1/2 proof) - the 205 quadrature terms, every finite enclosure, the whole error budget and every interval…
REFUSED	F-433	The Reconstruction Threshold for the Ferromagnetic Four-State Potts Model	decided in part (pre-registration amendment 5): the product inequality (b) is decided only on C x S, S x C and C' x C' (about 0.4% of S x S by volume; the rest projected above 20 CPU-hours at ~5 s per cell); the scalar certificate and…
REFUSED	F-435	The exact reconstruction threshold for the three-state symmetric channel	decided in part (pre-registration amendment 5): the interval certificate is decided only for q <= 4/5; q > 4/5, which holds the near-uniform corner where P ~ 2e-5, is not (extending band 2 to q <= 9/10 alone took 84,610 boxes and 1,916…
CERTIFIED	F-467	Routing densities and representation contraction for Thorp sweeps	a finite component: the five rational inequalities of Section 4 (H(1/8), H(13/50), H(1) and the two entropy brackets at 7/25 and 1) with every supporting finite fact the text states (closed form of h_j from its definition, h_j <=…
NEEDS DATA	F-532	The maximum number of mutually unbiased bases in dimension six	Algorithm and error analysis in build/sections/{seed,completion,phase-cover,refinement,exclusion,rounding,execution}.tex (5,886 tex lines). The code and data are NOT PUBLISHED in the clone: build/sections/execution.tex:16-20 names…
CERTIFIED	F-533	Exact Fourier certificates for complex Hadamard matrices of order six	a finite component: the exact finite core of both theorems — the single-matrix certificate (Prop. pair-certificate, both q), the finite arithmetic of the cubic-pair obstruction (Prop. cubic-exclusion), and the mixed-moment certificate…
REFUSED	F-539	The periodic spin-one Haldane gap	a finite component: the finite inputs of the two initializations — the trial MPS contractions at N = 72, 120 (exact U_N, V_N), the thermal recurrences (all nine t_{n,g} at b = 21/2 and W_{n,g} at b = 49/4 for n <= 11 recomputed exactly,…
CERTIFIED	F-540	A boundary-field gap for the spin-one Heisenberg chain	a finite component: the fifteen thermal integers k_{n,g} recomputed by the printed recurrence and every enclosure built on them (Y_6 < .027, c_0 P_*(lambda_0)^2 < .003745), the four trial-vector certificates (m = 34, 78, 142, 240)…
CERTIFIED	F-541	Uniform Stability of the Spherical Laughlin Gap	a finite component: this paper's restated seven-row certificate (Appendix A) — 13 three-body margins > 0 with the printed floors, M >= 0 exactly for D = 1..23 with the printed sign table, P^2 eta, 61/4096, 1222 and the final margin…
CERTIFIED	F-542	A Fock-space inequality and the Laughlin spectral gap	a finite component: the seven published rows give the 13 three-body margins of eq:3certificate (all > 0, floors as printed) and the 23 four-body certificates of eq:4certificate (M >= 0 exactly, sign table as printed), each re-derived from…
CERTIFIED	F-549	Entanglement with zero distillable secret key in local dimension ten	a finite component: the integer pencil and L (PPT), the twenty singular directions with every modular datum the paper prints, Phi_1 and Phi_2 PPT, Z PSD/PPT and nonzero with all twenty xhat x xhat in ker Z, rho = Z/tr Z in the class C,…
CERTIFIED	F-561	Full support of the zero-temperature Sherrington-Kirkpatrick order parameter	a finite component: the exact rational certificate of Lemma cert:identity-lemma (the identity, every printed constant and the positivity of all 22 remainder coefficients) and the pointwise algebra of Lemma shape:ibp; not the sign lemmas,…
REFUSED	F-605	The Kervaire invariant problem at the prime three	a finite component: the structure constants, the low-degree Ext groups D_{1,27} = <v^26 a, y, t_7'> and D_{6,10} = <v b^3> by an independent ordinary-cobar computation (matching the paper's printed checkpoints), the named cocycles and…
CERTIFIED	F-664	Three fixed points on the symplectic quadric threefold	a finite component: f(x,y) = e.x + (x-p).y on S^2 x S^2 has exactly three critical points, q_0 = (p,-e) degenerate (Hessian rank 2); NOT the passage to Hamiltonian fixed points on Q^3 nor Crit(Q^3) = 4
CERTIFIED	F-665	Zero-Plane Rigidity for Einstein Four-Manifolds	a finite component: every exact polynomial certificate the paper prints -- the appendix lemmas scalar (8 interval boxes), matrix-and-boundary (12 triangle rows) and potential F (20 interval boxes), with the polynomials re-derived from…
CERTIFIED	F-667	Positively curved Einstein four-manifolds	a finite component: every exact polynomial certificate the paper prints -- the appendix lemmas scalar (8 interval boxes), matrix-and-boundary (12 triangle rows) and potential F (20 interval boxes), with the polynomials re-derived from…
CERTIFIED	F-675	A finite-time singularity of Calabi flow on projective space	the whole of Proposition cert:shoot (existence on [0,56], 1 + p > 0, \|q\| <= .25R, \|\|(Re xi, Im xi) - z\|\| <= .13R for every z in the square), by an independent validated integration; not the tail lemma, the matching or the theorem
CERTIFIED	F-678	The Isoperimetric Conjecture for the Cubic Flat Three-Torus	a finite component: Proposition num:scalar-positive (B > 0 on [.64,1.02] u [1.62,2.25], B + S > 0 on [1.02,1.62]), decided independently, and the paper's knot and gap tables; NOT the geometric reduction to these inequalities
CERTIFIED	F-688	A counterexample to integer-degree harmonic dimension comparison	a finite component: the supplementary exact spectral selection at n = 16, k = 50000 (finite-selection.tex) — every parameter inequality, the eigenvalue data, the multiplicities, every square-root bound and the three printed integers; not…
CERTIFIED	F-699	The critical dimension for one-phase Bernoulli minimizers	a finite component: the exact arithmetic of Proposition cert:universal (the universal algebraic certificate behind the flatness half, d <= 6), from Tables I and II: the interior expansion with its 1714 keys and ten printed D_0 sums, D_0…
CERTIFIED	F-704	Stable self-similar blowup for a supercritical defocusing Schrödinger equation…	a finite component: every finite comparison of Appendix cert:arithmetic (integer box, boundary-form positivity, winding sign table and margins, high-angular polynomial, profile enclosures and degree comparisons, exterior positivity), and…

§5 · the release itself

Facts the census found

It moved. Two days after release, one commit withdrew 3 manuscripts (a sign error in one invalidated two dependent papers), revised 14 and added 11 challenges. The audit holds at fd4aeeb2; a later commit is a new pin.
Two kernels, two challenges. nanoda was enabled in 2 of 416 configs (412 false, 2 absent).
What the statements import. 386 challenges import all of Mathlib; 2 (declared supporting results) import OpenAI's own library, so their definitions come from the claimant.
One statement declares an axiom. HarmonicGrowth (mainStatement) — lane K decides whether the solution uses it.
Large statements. EditApproximation 19,170 lines, CoarseAssembly 6,649 lines, CKSBondiPenrose 3,597 lines; median 80 lines.
Coverage, counted our way. OpenAI states 300 of 719 top-line results formalized. Its scope notes link 339 current manuscripts; 242 of 372 families have at least one challenge.

§6 · limits

What this audit does not decide

Unformalized proofs. 362 manuscripts are linked by no scope note and carry no finite core: they are UNDECIDED HERE, which says nothing about whether they are right.
The analytic parts of finite-core papers. A certified finite component is the computation the paper says its argument needs; the argument itself is the paper's.
Readings. Lane S is two careful readings per contested family, quoted to the line — a reading, not a certificate.
Who wrote the checkers. The deciders and readings were produced in this session by parallel agents under one written brief, then run here; they are checked by their forges, by every printed number they reproduce and by the second readings — not by a second independent implementation.