Paper deep dive
What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics
Ying Xie
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:On 6 October 2026 OpenAI published an initial 722 AI-written mathematical manuscripts, organized into 372 problem families, in the public repository this http URL. The release includes claimed solutions to many prominent open problems. We approach this collection as a treasure mine of mathematical ideas. Our aim is to extract new lemmas, constructions, inequalities and proof mechanisms introduced in the source arguments, and to distinguish them from established tools and new combinations of those tools. We call these mathematical instruments. Extraction comes first; their validity, novelty and possible reuse then become subjects for further study. The resulting descriptions also help readers understand the selected papers without having to reconstruct every argument at the outset. We examine 38 families in two groups of 17 and 21, spanning number theory, geometry, analysis, combinatorics, complexity, algebra, operator algebras, topology and mathematical physics. Each entry records the claim, extracted instruments, antecedents and caveats. Eleven cross-cutting patterns connect the entries, and a scoreboard records formalization status and dependencies. Novelty assessments are provisional and sometimes mixed. Selected source comparisons correct mathematical statements, hypotheses and counts; they do not independently establish priority or certify the underlying proofs. No Lean development was compiled or kernel-checked for this survey. We also briefly describe a subsequent application of the signed restriction lemma from family 112 to circuit lower bounds at every fixed depth.
Tags
Links
- Source: https://arxiv.org/abs/2610.17090v1
- Canonical: https://arxiv.org/abs/2610.17090v1
Trouble viewing inline? Open PDF directly â
Full Text
189,283 characters extracted from source content.
Expand or collapse full text
What the Machine Invented: Mining New Mathematical Instruments from OpenAIâs October 2026 Release of AI-Generated Mathematics Ying Xie Affiliation: Kennesaw State University Email: yxie2@kennesaw.edu October 2026 Abstract On 6 October 2026 OpenAI published an initial 722 AI-written mathematical manuscripts, organized into 372 problem families, in the public repository github.com/openai/math [1]. The release includes claimed solutions to many prominent open problems. We approach this collection as a treasure mine of mathematical ideas. Our aim is to extract new lemmas, constructions, inequalities and proof mechanisms introduced in the source arguments, and to distinguish them from established tools and new combinations of those tools. We call these mathematical instruments. Extraction comes first; their validity, novelty and possible reuse then become subjects for further study. The resulting descriptions also help readers understand the selected papers without having to reconstruct every argument at the outset. We examine 38 families in two groups of 17 and 21, spanning number theory, geometry, analysis, combinatorics, complexity, algebra, operator algebras, topology and mathematical physics. Each entry records the claim, extracted instruments, antecedents and caveats. Eleven cross-cutting patterns connect the entries, and a scoreboard records formalization status and dependencies. Novelty assessments are provisional and sometimes mixed. Selected source comparisons correct mathematical statements, hypotheses and counts; they do not independently establish priority or certify the underlying proofs. No Lean development was compiled or kernel-checked for this survey. We also briefly describe a subsequent application of the signed restriction lemma from family 112 to circuit lower bounds at every fixed depth. Contents 1 Introduction 2 Background and motivation 2.1 The challenge of reading a large release 2.2 Extracting the instruments within the proofs 2.3 Why this matters 2.4 What the extraction does not do 3 The extraction at a glance 4 Method, and what ânewâ means here 5 The map 6 The map, second group 7 Cross-cutting patterns 7.1 Existence instead of construction 7.2 Estimates become extremal problems 7.3 Entropy and information as proof devices 7.4 Parity and characters over finite fields 7.5 Rigidity theorems that erase regularity hypotheses 7.6 Established methods in new settings 7.7 Rediscovery without citation 7.8 Consequences and proposed extensions 7.9 Probability imported into deterministic problems 7.10 Auxiliary structure manufactured by the proof 7.11 Label versus content 8 Family by family 8.1 Number theory and arithmetic geometry 8.1.1 003 ¡ Zero-free half-plane ReâĄs>7/8Res>7/8 8.1.2 004 ¡ Hilbertâs tenth problem over âQ 8.1.3 017 ¡ Irrationality exponent of Ď is 2 8.1.4 032 ¡ Rational Hodge conjecture for CM abelian varieties 8.2 Analysis and geometry 8.2.1 074 ¡ Kakeya maximal conjecture in â3R^3; Kakeya sets in â4R^4 8.2.2 087 ¡ The Mahler conjectures 8.2.3 362 ¡ Relativistic VlasovâMaxwell, 3D, large data 8.2.4 304 ¡ HilbertâSmith conjecture in every dimension 8.3 Combinatorics and theoretical computer science 8.3.1 102 ¡ Unique Games Conjecture 8.3.2 107 ¡ Matrix multiplication exponent Ďâ¤9/4Ď⤠9/4 8.3.3 157 ¡ Counterexample to Hadwigerâs conjecture 8.3.4 158 ¡ The plane is not 5-colorable 8.3.5 159 ¡ ErdĹsâs reciprocal-sum conjecture 8.4 Algebra and operator algebras 8.4.1 196 ¡ Counterexample to Kaplanskyâs zero-divisor conjecture 8.4.2 197 ¡ Counterexample to Kaplanskyâs direct-finiteness conjecture 8.4.3 248 ¡ Thompsonâs group F is not amenable 8.4.4 287 ¡ All free group factors are isomorphic 9 Family by family, second group 9.1 Number theory and arithmetic geometry 9.1.1 002 ¡ Full BSD formula from low Selmer corank 9.1.2 007 ¡ Ordinary two-point Chowla 9.1.3 010 ¡ FontaineâMazur modularity at the prime 2 9.1.4 040 ¡ Blochâs conjecture for surfaces with pg=0p_g=0 9.1.5 193 ¡ Serreâs positivity conjecture 9.2 Analysis, dynamics and mathematical physics 9.2.1 143 ¡ Hilbertâs sixteenth problem, uniform bounds 9.2.2 263 ¡ The ionization conjecture 9.2.3 265 ¡ Two-dimensional area law from a global gap 9.2.4 268 ¡ The spin-one Haldane gap 9.3 Combinatorics, geometry and complexity 9.3.1 103 ¡ L=RL=BPLL=RL=BPL 9.3.2 112 ¡ Depth-three circuits beyond the square root 9.3.3 156 ¡ Borsukâs conjecture fails in dimension 9 9.3.4 266 ¡ Three mutually unbiased bases in dimension six 9.4 Operator algebras, topology and symplectic geometry 9.4.1 221 ¡ MĂŠzardâParisi formula for diluted spin glasses 9.4.2 285 ¡ BaumâConnes and KadisonâKaplansky counterexamples 9.4.3 293 ¡ Hyperinvariant subspaces and transitive algebras 9.4.4 297 ¡ Naimarkâs problem in ZFC 9.4.5 309 ¡ Kervaire invariant at the prime three 9.4.6 325 ¡ The complete Crouzeix conjecture 9.4.7 340 ¡ Counterexample to the nearby Lagrangian conjecture 9.4.8 376 ¡ Universal computation in forced NavierâStokes flows 10 Verification and dependency scoreboard 11 Limits of the extraction and mathematical review 12 Conclusion and future directions Acknowledgments References 1 Introduction OpenAIâs release brought together hundreds of manuscripts addressing longstanding mathematical problems: the Unique Games Conjecture, the exponent of matrix multiplication, Hadwigerâs conjecture, the chromatic number of the plane, Kaplanskyâs conjectures, the amenability of Thompsonâs group F, the isomorphism problem for free group factors, and many others. Several are accompanied by Lean formalizations; most are not. None had been peer-reviewed at the time of writing. The motivation for this project is to treat the release as a source of mathematical ideas. A proof is more than a certificate that its theorem is true: it is a store of methods. When a long proof of a famous conjecture is correct, the devices that make it work can have value beyond the theorem; even when an argument fails, a lemma or construction within it may remain valid. The purpose of this project is to mine the release for those devices. We call them instruments: new objects, structures, inequalities or proof architectures that a proof introduces in order to reach its conclusion, together with new settings in which established tools are applied. The project has two goals. (i) Extracting new instruments. To isolate and describe the new lemmas, constructions and proof mechanisms generated in these arguments. Once their statements, proofs and relation to earlier work are understood, they can contribute to the shared mathematical knowledge base. (i) Making the source arguments accessible. To give readers a consistent account of what each selected paper claims, which instruments it introduces, which established results it uses, and which steps require closer examination. A case study in reuse. After extraction, we investigate whether particular instruments can be reused. A separate application manuscript studies the signed restriction lemma identified in family 112. The lemma controls correlations through signed combinations of narrow CNFs with bounded expected coefficient mass. Combining it with adaptive averaging, classical depth reduction and quantitative sparsification yields, for the same polynomial-time language as in the source, the gate-count lower bound SDâ(fn)âĽ2ΊDâ((nâlogâĄn/logâĄlogâĄn)1/(Dâ1))for every fixed âDâĽ3S_D(f_n)⼠2 _D ((n n/ n)^1/(D-1) ) every fixed D⼠3 at all sufficiently large input lengths n. Here SDS_D counts AND/OR gates in exact circuits of depth at most D, with arbitrary finite fan-in and fan-out and input negations. The source supplies the lemma and the language; the application extends the sourceâs stated depth-three result. The proof will be presented in the separate application paper. This case illustrates the progression from extracting an instrument to investigating its use and obtaining a further theorem. What this paper contains. We report an extraction and preliminary novelty assessment for 38 families, selected for the prominence of their problems. For each family, the initial extraction examined the source argument to identify candidate new instruments and distinguish them from combinations of known tools. The paper contains: ⢠a map of the 38 families (Tables 2 and 3), giving for each the result, its Lean status, its central extracted instrument and a provisional novelty assessment; ⢠eleven cross-cutting patterns (Section 7) describing recurring approaches in the source proofs, from âexistence instead of constructionâ to âestablished methods in new settingsâ and ârediscovery without citationâ; ⢠family-by-family cards (Sections 8 and 9) that state each claim, describe the selected candidate instruments with section and lemma references, list what is reused, and record caveats; ⢠a verification and dependency scoreboard (Section 10) recording formalization status, statement faithfulness, dependence on other OpenAI manuscripts, and uncited nearest ancestors; ⢠an explicit account of the limits of the extraction and mathematical review (Section 11). Status of the results. Throughout, âthe paper provesâ and similar phrases describe what a manuscript claims and how its argument is organized. The manuscripts have not been peer-reviewed. Formalization statuses are those recorded during the initial extraction as of 11 October 2026, with the source-status corrections noted below. No Lean project was compiled during either stage. Verdicts of novelty mean ânew relative to the citable literature examined during the initial extractionâ, not established priority. 2 Background and motivation 2.1 The challenge of reading a large release A release of this size poses several practical difficulties for readers: ⢠Volume. Some manuscripts run to 170â200 pages, and several families contain closely related papers. Reading even a selected part of the release requires substantial time. ⢠Technical density. Many arguments involve nested limits, numerous parameters, and compactness or ultrafilter constructions. Identifying the central mechanism can require tracing dependencies across many sections. ⢠No peer review. The manuscripts have not passed through the ordinary refereeing process, and the repositoryâs own formalization catalogue marks review status âuncheckedâ. ⢠Need for accessible descriptions. A short account of an instrument can help readers decide where to begin in a long source argument, while leaving the correctness of that argument to further examination. These difficulties make structured descriptions useful: they provide starting points for reading, comparison and verification. 2.2 Extracting the instruments within the proofs The project begins with the mathematical content inside each selected argument. We identify the objects, lemmas and proof mechanisms it introduces, trace their roles in the proof, and compare them with earlier work. The family entries present the results of that extraction in a common format. Whether a particular instrument can be used elsewhere is a subsequent question, illustrated by the application described in the introduction. 2.3 Why this matters We see several ways in which a structured extraction of this kind can be useful beyond the immediate question of which claims are correct. Some benefits concern access to the source arguments; others, including further mathematical applications, depend on the validity of the instruments concerned. (1) A catalogue of extracted instruments. Instruments are described in a form detached from their headline theorems: for example, a âshared-leg entropy inequalityâ for points of Strassenâs asymptotic spectrum (107), a âlatent alphabet gadgetâ with noise that rarely changes the honest decoderâs output (102), âtriangular polynomial cellsâ with descending precision budgets (159), or a âcoupled purity bootstrapâ as a spectral-gap criterion (268). Their statements and proofs can be studied separately from the headline claims before possible applications are investigated. (2) Cross-field transfer of mechanisms. One recurring pattern is âestablished methods in new settingsâ (Section 7): a published theorem applied in a setting for which the initial comparison found no precedent, such as the BenyaminiâSternfeld fixed-point-free Lipschitz map against amenability, Bravermanâs theorem on bounded-depth circuits for Chowla, or Quot-scheme localization for Blochâs conjecture. Describing these transfers gives readers concrete examples to investigate in other settings. (3) Directing verification effort. The cards and scoreboard identify steps on which the conclusions depend, dependencies on other unverified manuscripts, and gaps in the formalization coverage inspected. These details help a reader choose which statements or arguments to check first. (4) Reducing the cost of initial reading. A short entry introduces a manuscript that may extend to two hundred pages. It points to the proposed new instruments and distinguishes them from established ingredients, giving a specialist a route into the full proof. (5) A method for examining further releases. The same extraction method can be applied to other large collections. A fixed protocol (one AI reading per family, usually up to three candidate devices traced through the proof, a literature search per device, a four-grade verdict, and an explicit list of caveats and dependencies) is a template that the community can apply, extend, and audit in turn. (6) Scaffolding for formalization. By isolating the exact statement, the load-bearing lemmas, and the external and internal dependencies of each result, the extraction indicates where formalization effort should be directed, and which existing formal developments still require independent compilation and kernel re-checking. 2.4 What the extraction does not do The extraction is not a verification of the source proofs; selected statements and identities were checked. Its novelty assessments are limited by the literature examined, and fresh searches were not completed for every family in the second group. The selection covers 38 of 372 families and favors prominent problems. The instruments identified here are devices within proofs; the extraction did not identify a new foundational theory comparable in scope to motives or perfectoid spaces. Section 11 gives the full limits of the extraction and mathematical review. 3 The extraction at a glance OpenAI math release ¡ 6 Oct 2026 ¡ extraction from 38 selected families. The selected set contains thirty-eight family entries, in groups of seventeen and twenty-one. The initial extraction asks which instruments appear new and which combine known tools. The tables retain its qualitative verdicts, with corrected theorem statements and explicit limits on verification. Quantity Value Note Families examined 38 selected for the prominence of the problem, across number theory, geometry, analysis, combinatorics, complexity, algebra, operator algebras, topology and mathematical physics. Group 1: 17 families. Group 2: 21 families Novelty classifications qualitative Mixed labels are retained at the family and instrument level. No disjoint numerical breakdown is asserted, and novelty judgments have not been independently validated by the subsequent mathematical review Original headline-formalization labels 19 of 38 Includes partial inspection for 003 and 087. Five other original entries were companion-only, counting 159. These are labels from the initial extraction; source-status corrections and the counting rule appear in Section 10. No Lean build was run Recurring pattern Established methods in new settings a 1983 theorem on maps without approximate fixed points is applied to amenability; a 2009 circuit-complexity theorem to Chowla correlations; Quot-scheme localization to Bloch; a 2019 conformal map to Mahler Table 1: Summary figures of the extraction (as of 11 Oct 2026). 4 Method, and what ânewâ means here The work proceeded in two stages. The initial extraction identified candidate mathematical instruments, compared them with the literature, and assigned preliminary novelty assessments. The subsequent mathematical review checked the reported theorem statements and selected supporting arguments and revised the draft. These terms distinguish the two activities throughout the paper. Both groups of familiesâthe first 17 and the second 21âbelong to the initial extraction. During the initial extraction, a separate AI reading was carried out for each family, using the LaTeX source where the repository provides it (most do, under build/sections/), otherwise the PDF, together with the Lean challenge and solution files and, where released, the abridged reasoning trace. Each reading generally isolated up to three candidate devices, traced each through the proof, then searched the literature for the device and its nearest relatives. Verdicts use four grades. New an object, structure, inequality or proof architecture with no precedent found, even though its parts are classical. New combination the ingredients are established, while their combination or application appears new. Incremental a refinement or variation of an established technique. Unclear the available text and comparisons did not support a definite classification. The subsequent mathematical review compared theorem statements and selected supporting arguments against a pinned repository snapshot and corrected mathematical statements, hypotheses and counts. Potential extensions, including the proposed logarithm analogue of family 017, are distinguished from consequences actually established here. Literature comparisons and novelty assessments originate in the initial extraction; the subsequent mathematical review did not repeat every search. Literature-search coverage varied across the two groups. For some entries in the second group, comparison relied on directly retrieved primary sources and the modelâs existing knowledge without a fresh search. The affected entries identify this limitation. These comparisons are not an exhaustive prior-art search. 5 The map Table 2: The map, first group: 17 families. Family Result Lean Central extracted instrument Verdict 003 Îś and Dirichlet L zero-free for ReâĄs>7/8Res>7/8 partial inspection Twist the MĂśbius sum by all sextic residue symbols; Poisson fuses Îź with Gauss sums into cubic Gauss sums, whose KubotaâPatterson automorphy moves the thin sextic family to a quadratic one where square-root cancellation on average is known. combination as architecture, leaning new 004 Hilbertâs tenth problem over âQ undecidable no The reduction does not construct a Diophantine definition of â¤Z. A Turing reduction dovetails integer-root enumeration with finite rational-oracle tests. Compactness and elliptic height bounds show that some finite test fails if no integer root exists. Every terminating run makes finitely many queries, with no uniform bound asserted. new 017 Irrationality exponent of Ď equals 2 yes âSeparated-weight interpolationâ: jets at translates on the exponential curve with anisotropic weights chosen independently of the centers, while the sufficiently large degree threshold may depend on them, proved by a Dyson-type curve inequality pushed through nef/ample and Serre vanishing on a weighted blow-up. combination bordering new 032 Rational Hodge conjecture for CM abelian varieties no âFixed-input variationâ: freeze the theta-series input on a Picard-type ball quotient, move only the definite-place complex structure, keep a (2,0)-form period nonzero, then rationalize by weak approximation. combination 074 Kakeya maximal conjecture in â3R^3; Kakeya sets in â4R^4 have dimension 4 no Differentiate the critical exponent: BV gives approximate differentiability of the exponent surface; a separate monotonicity argument yields an ordinary differentiability point whose partial derivatives prescribe extremal configurations ruled out by an entropy and mutual-information bound. In 4D, a variational âhorizonâ built from quadratic local fits replaces polynomial Wolff axioms. combination leaning new; 4D framework new 087 Mahler conjecture, symmetric and general symmetric Replace each real strip by a complex lens with uniform boundary coordinate (Grossâs conformal Skorokhod map); push Lelong-number Jacobian mass to the boundary as kââkââ; the volume product becomes a sum of feasibility probabilities over signed simplices packing inside the polar. new feasible-simplex identity; rest combination 102 Unique Games Conjecture yes âLatent alphabet gadgetâ: a nonlinear shift-equivariant decoder on a big latent space with a noise law that rarely changes the honest decoder but is detected by every linear family with sufficiently large rank on the output subspace, so the degree-two KMS inverse theorem applies unchanged. new 107 Matrix multiplication exponent Ďâ¤9/4Ď⤠9/4 yes The proof bounds every point of Strassenâs asymptotic spectrum using polynomial multiplication, without giving a matrix-multiplication algorithm: a DFT-over-copies degeneration keeps all blocks sharing a leg and yields a âshared-leg entropy inequalityâ; concavity plus tripling force growth a4/3a^4/3. new as a proof of an Ď bound 157 Counterexample to Hadwigerâs conjecture yes Algebraic âhole relationâ: non-edges certified by a symmetric bilinear identity whose terms cancel around any triangle leaving 0=10=1, so the complement is triangle-free. Connected matchings are excluded by an entropy-minimizing container argument. new 158 The plane is not 5-colorable yes âTransfer of colorabilityâ: a proper k-coloring exists iff a weak measurable one does, via a rigidity theorem that every wild rotation-invariant law on the dual of the algebraic plane is Haar. The only finite graph used is a Moser spindle in the final step. new 159 ErdĹs reciprocal-sum conjecture; quasipolynomial SzemerĂŠdi original: companion only; see card âTriangular polynomial cellsâ with descending precision budgets: a density increment that never resets to a sub-progression; the loss at weight i depends only on precisions at higher weights, turning logâĄlogâĄN N into logâĄN N. new architecture 196 Counterexample to Kaplanskyâs zero-divisor conjecture yes Projective-plane label sets with pairwise odd intersections make every vertex of the âsimultaneous-stepâ product graph odd-degree, so every component is even and the product vanishes mod 2. Collapse is excluded by a girth-conditioned random-matching estimate plus a LiptonâTarjan reduction of planar pairings. combination; separator step new 197 Counterexample to Kaplanskyâs direct-finiteness conjecture; a non-sofic group as a consequence yes An âincidence criterionâ: a hypergraph of degree â+1 +1 and girth 12 plus vectors with block-sum 0 and total âI-I yields aâb=1,bâaâ 1ab=1,\ baâ 1 after gluing copies of â2F_ ^2, averaging, character-twisted HNN packing, and a homomorphism to the field that exposes a rank-deficient Gram matrix. new criterion; parts combination 248 Thompsonâs group F is not amenable yes Color each element of a Følner set by a Hilbert-ball vector via the recursion âcolor = f(average of child colors)â, with f a BenyaminiâSternfeld Lipschitz map having no approximate fixed point; pair transports force the averages to agree, an impossibility. new use; leaning new 287 All free group factors isomorphic; fundamental group â+R_+ yes âSmall cocycle with a prescribed word valueâ: a Fox-derivative cocycle â2 ^2-tiny on each generator that accumulates a full unitary factor on a long word with free prefixes, because spectral cutoffs of the prefix-sum operator give approximate inverses in the required vector norm (the limiting free Poisson law has no atom at 0). A trace-preserving flow then absorbs a generator. combination 304 HilbertâSmith conjecture in every dimension no Witt-group âsignatureâ of a sphereâs orientation form pushed through the wild orbit space into a test sphere, in âcompact-source test categoriesâ of sheaves built from arbitrary continuous maps; denominators bounded by a lattice fixed before any action data; a faithful â¤pZ_p action splits it into pkp^k equal integral pieces. new 362 3D relativistic VlasovâMaxwell, large data, global smooth yes âSigned momentum incrementâ bootstrap: bound the net impulse on a particle over a short interval, not the force pointwise, via a signed LiĂŠnardâWiechert identity along source worldlines; each momentum doubling costs time âĽc/logâĄP⼠c/ P, and the harmonic sum diverges. combination; direction-change counting new 6 The map, second group Table 3: The map, second group: 21 families. Family Result Lean Central extracted instrument Verdict 002 Full BSD formula in Selmer corank 0 and 1 no âTame variablesâ: ultrafilter limits of cyclic characters at auxiliary primes used as extra Iwasawa variables to force integrality with no residual-image hypothesis; a âtheta implicationâ comparing Artin lengths from a holomorphic theta family on U(3,1) with a nilpotent parameter replaces Eisenstein congruences. new construction; rest combination 007 Ordinary two-point Chowla; corrected binary Elliott original: statements only; see card âTerminal-scale divisor binsâ: dilations confined so narrowly that the scale is unchanged, removing Taoâs logarithmic averaging; integers certified to behave like independent residues by Bravermanâs theorem that polylog independence fools AC0AC^0. combination bordering new 010 FontaineâMazur modularity at p=2p=2, all residual types no âMarked linesâ: after a huge abelian 2-extension, record an ordinary line at only a vanishing fraction of dyadic places, enough to force the residual fiber connected while leaving the propagation step unrestricted at 2. combination 040 Blochâs conjecture for all surfaces with pg=0p_g=0 no Apply virtual enumerative geometry to a Chow problem: a torus-localized Quot-scheme count with two copies of the surface left unintegrated vanishes for degree reasons, so fixed loci give a diagonal decomposition with a universal coefficient; for fake projective planes the coefficient is read on a CartwrightâSteger surface. new strategy 103 L=RL=BPLL=RL=BPL yes âExact correction and copy hierarchyâ: no pseudorandom generator; refine the configuration graph algebraically so every transition weight is small, estimate the reward with a sampler driven by one O(log n)-bit environment, and control the evaluatorâs recursive space use with a catalytic key-equality gadget. new 112 Explicit depth-3 circuit lower bound 2ĎâĄ(n)2^Ď( n) yes âRestriction bound independent of clause countâ: a restricted width-k CNF written as a signed combination of width-b CNFs with bounded expected mass, with a suitable testing width for any fixed pâkpk; the standard switching bound (5âpâk)s(5pk)^s gives decay in s when pâk<1/5pk<1/5. new 143 Hilbertâs 16th: HâĄ(n)<âH(n)<â for every degree no (companion only) Parametric LionâRolin preparation of the slope field, coefficients as parameters, in place of blow-ups, giving a finite alphabet of passages uniform over degeneracies; a Khovanskii-type projection principle turns non-uniform finiteness into a uniform bound; Ilyashenkoâs cochains re-engineered into multi-scale âpacketsâ. combination 156 Borsukâs conjecture fails in dimension 9 yes The set of rank-one projectors of â4R^4 (a copy of ââP3RP^3 in â9R^9) needs at least 11 pieces: an âodd spectral extensionâ turns any 10-cover into an odd map between 9-spheres, and degree analysis at the tight BorsukâUlam bound forces a 10-vertex ââP3RP^3-like complex that cannot exist. combination leaning new 193 Serre positivity in ramified mixed characteristic no âRank quotientâ: sequences of finite-length modules along the p-power-root tower modulo negligible normalized rank, packaged as perfect complexes over a connective algebra so K-theoretic descent acts on asymptotic perfectoid data; ordinary and perfectoid Euler characteristics compared only after Galois norms. new device 221 MĂŠzardâParisi formula for diluted spin glasses yes (not in catalogue) âDepth shiftâ: couple to a finite auxiliary hierarchy by marked Poisson perturbations and shift every target branching depth by one level so divisions by small coefficients stay bounded, proving the factorization Panchenko left open. new 263 Ionization conjecture, full SchrĂśdinger theory companions only Condition a many-body ground state on noisy, unlabeled coarse-grained observations of electron positions; the energy cost is logarithmic in the event probability and free of particle number, so local failures of ThomasâFermi yield low-energy states that contradict semiclassics. new 265 2D area law from a global gap, frustration allowed no âOptimized nested positive filtersâ whose only cost is excitation energy, and âreplica metric transportâ encoding conditional mutual information as the derivative of a log-norm comparable to energy, with a displayed information term linear in the transport parameter and additional energy cost quadratic in that parameter and linear in the split probability. new 266 Exactly three MUBs in dimension six headline no; NâĄ(6)â¤5N(6)⤠5 yes Represent every order-6 complex Hadamard matrix by nine seed phases plus a U(2) polar factor, giving a finite cover of the unclassified continuum; the headline claim uses a binary64 computation with hand-proved margins. Companion: âinjective momentsâ calculus establishing Fourier vanishing outside Taoâs S6S_6 equivalence class. combination 268 Haldane gap for the spin-1 Heisenberg ring no âCoupled purity bootstrapâ: one partition function written as Gibbs weights and as powers of spatial transfer eigenvalues; squaring one doubles inverse temperature, squaring the other doubles length, and exact identities couple them. The criterion does not require frustration-freeness. new criterion 285 Reduced BaumâConnes injectivity fails (torsion-free) no âHeisenberg voltage towerâ: relators are nilpotent-group covers of an expander tower so each layer carries â2â(H) ^2(H) and incidence operators realize Bott-class symbols; an Eilenberg swindle makes the embedded torus class vanish. combination 293 No hyperinvariant subspace; transitive algebra problem yes âBackward intertwiner over an ergodic baseâ: unicellular weighted shifts glued over the 2-adic odometer; multipliers force a tail index per fiber, a commuting operator lowers it along orbits, and a finite integer-valued measurable label cannot strictly decrease almost everywhere under a measure-preserving map. new 297 Naimarkâs problem in ZFC yes (not in catalogue) âSelective bridgeâ: a reduced HNN adjunction along peaking projection sequences merges exactly two pure-state classes while every other pure state extends uniquely, so each step depends on countably many earlier ones and diamond is replaced by cardinal bookkeeping at length + c^+. combination 309 Kervaire invariant at p=3p=3: survivors exactly jâ0,2,3jâ\0,2,3\ no âFinite Euler boundâ: a coordinate-change coefficient as a nilpotence witness imposes a deadline on the Tate spectral sequence, replacing the Gap and Periodicity theorems of HillâHopkinsâRavenel; the BelmontâRay coefficient model is proved along the way. combination 325 Complete (matrix-valued) Crouzeix conjecture yes âOrdered density comparisonâ: compress the CrouzeixâPalencia positive kernel by the top singular pair into a 2Ă22Ă 2 block of boundary matrix functions and measure in HilbertâSchmidt norm, so Parseval over Faber coefficients replaces the triangle inequality that gave 1+21+ 2. combination leaning new 340 Counterexample to the nearby Lagrangian conjecture no âMomentum separationâ: a generating family with an exponential scale over the parameter sphere upgrades the immersed Legendrians of the 2026 Ălvarez-GavelaâIgusaâSullivan program to an embedded exact Lagrangian; the obstruction is a 2-torsion class in Waldhausenâs stable tube space. combination 376 Universal computation in forced NavierâStokes flows lemmas only Defining the force as the residual enforces NavierâStokes for a chosen smooth divergence-free flow; the required mean, regularity and time-dependence of that force still need proof; the construction is Mooreâs generalized shifts plus Bennett reversibility plus Hamiltonian box-moving. The extracted construction uses scale-nested memories under rapidly vanishing forcing. incremental 7 Cross-cutting patterns Several approaches recur across the selected proofs. The following patterns describe how the arguments establish existence, control parameters, transfer results between settings, and introduce auxiliary structures. They provide a way to compare instruments arising in different subjects. 7.1 Existence instead of construction Several arguments establish existence through compactness, spectral duality, random sampling, or a terminating search whose output has not been computed. The resulting existence statement need not supply an object of practical size. The proof of Ďâ¤9/4Ď⤠9/4 bounds the asymptotic spectrum without providing a competitive finite matrix size. The Hadwiger argument selects m through an ultrafilter, and the Hilbert 10 reduction uses a nonstandard root. The zero-divisor and direct-finiteness constructions use random choices or searches with parameters such as q=2217q=2^217 and nâłe300000n e^300000. In the second group, the Hilbert 16 argument gives an ineffective B(d), the nearby-Lagrangian example has no explicit dimension, and the Borsuk construction supplies a continuous set without extracting a finite subset. These examples differ in effectivity, but each leaves some construction data unspecified or unevaluated. 7.2 Estimates become extremal problems A proposed inequality can be studied through the regularity of its optimal-exponent function. Assuming that the desired bound fails, differentiation of this function imposes conditions on an extremal configuration. The proof then rules out a configuration satisfying those conditions. In the three-dimensional Kakeya argument, coordinatewise monotonicity gives local BV regularity and approximate differentiability almost everywhere. An additional monotonicity comparison yields ordinary total differentiability, and the partial derivatives determine the relevant plank shapes. The four-dimensional argument uses a âhorizonâ defined by an infimum over quadratic fits. In the ErdĹs argument, a potential controls the loss at each weight using only the higher weights. 7.3 Entropy and information as proof devices Mutual information, relative-entropy projections, and entropy inequalities organize estimates in several proofs. The information quantities measure how much dependence or conditioning is available, and incompatible upper and lower bounds produce a contradiction. The Kakeya proof uses a mutual-information bound to apply a projection theorem to dependent events. The Hadwiger construction combines KleitmanâWinston recording with a CsiszĂĄr I-projection as its progress measure and a FordâFulkerson cut as its stopping certificate. The matrix-multiplication argument for Ď uses an entropy inequality for a shared tensor leg, while the zero-divisor construction bounds repeated traversals of a random graph by entropy. In the second group, conditioning in the ionization argument costs log5âĄ(e/p) ^5(e/p) times the inverse squared noise scale in energy. The area-law proof expresses conditional mutual information through a log-norm derivative, and the Haldane-gap proof uses a RĂŠnyi-2 purity bootstrap. 7.4 Parity and characters over finite fields Four constructions use cancellation in finite fields, either through a scalar identity or through vanishing character sums. The direct-finiteness construction requires â+1=0 +1=0 in K. The zero-divisor construction uses projective lines whose pairwise intersections have odd size. The UGC gadget is defined over 2sF_2^s and contains a quadratic block over 2dF_2^d. The proof of Ďâ¤9/4Ď⤠9/4 applies a DFT across L=5âML=5M copies to select exactly the matching labels. 7.5 Rigidity theorems that erase regularity hypotheses Some arguments replace a regularity assumption with a transfer theorem. The theorem connects the unrestricted object to a measurable, constructible, or otherwise controlled formulation, so that the remaining proof can use that formulation. For plane coloring, the transfer states that a proper coloring exists exactly when a weak measurable coloring exists. The HilbertâSmith argument uses sheaf categories generated by arbitrary continuous maps from polyhedra while retaining invertible Verdier duality. The Hilbert 10 argument uses an oracle reduction without constructing a definable copy of â¤Z. 7.6 Established methods in new settings A recurring contribution is the application of an established theorem in a different mathematical setting. The relevant novelty question concerns that application and its surrounding argument; the imported theorem retains its original attribution. The examples include the BenyaminiâSternfeld theorem of 1983 on Lipschitz maps without approximate fixed points in an amenability argument; Grossâs 2019 conformal Skorokhod map in the Mahler proof; and KubotaâPatterson cubic theta theory from 1977 in a zero-free-region argument. Other transfers use Fox calculus and free Poisson laws for free group factors, Lelong numbers for volume products, and LiptonâTarjan separators for diagrams of van Kampen type. The second group applies Bravermanâs 2009 AC0AC^0 theorem to Chowla correlations, MarianâOpreaâPandharipande localization to Blochâs conjecture, LionâRolin preparation to Hilbertâs 16th problem, Uedaâs reduced HNN extensions to Naimarkâs problem, Suzukiâs quantum transfer matrix to the Haldane gap, and KuboâAndo means to the area law. 7.7 Rediscovery without citation The initial comparison identified several constructions closely related to earlier work that was not cited in the manuscript. In some cases, the corresponding reasoning summary does name the earlier source. These comparisons matter when distinguishing a new instrument from a reconstruction or adaptation. The VlasovâMaxwell manuscript uses a time-integrated momentum increment related to CheverryâIbrahimâs work, which is cited six times in the reasoning summary but absent from the paper. The interpolation argument for Ď has antecedents in Masser and FischlerâNakamaye; the spectral argument for Ď follows a template in AlmanâLiâs 2026 âStrassen calculusâ; and the Kakeya comparison identifies RiosâSawyer as an uncited antecedent. In the second group, the MĂŠzardâParisi reasoning summary names MourratâPanchenko and BarbierâPanchenko, while the paper omits them. The Serre-positivity argument uses an orbit lemma of SuslinâVoevodsky without citation. 7.8 Consequences and proposed extensions Some entries describe consequences of the stated results or suggest extensions beyond them. Each requires its own hypotheses and argument. The cards distinguish consequences presented as following from the source from adaptations that still need a proof. The centers (rj,jâpi/qi)(r^j,jp_i/q_i) suggest a possible analogue of the Ď argument for rââ>0â1r _>0 \1\. Establishing ÎźâĄ(logâĄr)=2Îź( r)=2 would require a separate interpolation, height and determinant argument; it does not follow verbatim from the theorem surveyed here. The claimed free-group-factor isomorphism would refute the ConnesâShlyakhtenko L2L^2-Betti conjecture for LâĄ(n)L(F_n), a consequence not discussed in the paper. In the second group, the hyperinvariant-subspace counterexample would also refute Kadisonâs transitive-algebra problem, which the catalogue summary omits; the MĂŠzardâParisi lower bound is stated for bounded interactions with permutation-invariant law, odd arity included. 7.9 Probability imported into deterministic problems Several proofs introduce a random or ergodic auxiliary system into a deterministic problem. Almost-sure statements or measure-zero obstructions in that system then support the deterministic conclusion. In the hyperinvariant-subspace construction, operators are assembled over the 2-adic odometer, where a finite integer-valued measurable label cannot strictly decrease almost everywhere along the measure-preserving dynamics. The ionization argument smooths and conditions electron positions. Marked Poisson perturbations provide the hierarchy in the MĂŠzardâParisi proof, while the BaumâConnes construction uses a local-lemma probability law along an infinite tower. The plane-coloring argument uses Haar rigidity for the unrestricted laws considered there. 7.10 Auxiliary structure manufactured by the proof An argument may introduce auxiliary structure with properties it can control, and then prove that the original object is constrained by that structure. The UGC construction introduces a latent alphabet hidden from the honest player. The proof of L=BPLL=BPL uses one shared O(log n)-bit environment for all samplers. In the MĂŠzardâParisi argument, a finite auxiliary hierarchy is refined only after NââNââ. The ionization proof uses a decreasing chain of observation Ď-fields. The BSD argument introduces tame Iwasawa variables and specializes them to zero at the end. 7.11 Label versus content A title may suppress restrictions that are essential to the mathematical statement. The extraction therefore records the precise model, hypotheses, and conclusion, including computational assumptions where they occur. âUniversal computation in NavierâStokesâ uses volume-preserving flows and a force defined by the residual; the prescribed forcing properties, including eventual stationarity, remain mathematical constraints to verify. âBaumâConnes counterexampleâ is reduced, coefficient-free rational injectivity for a finitely generated group; finite presentation is not determined, and the claim does not refute the classical Novikov conjecture. âThree MUBs in dimension sixâ rests on a binary64 computation conditional on compiler semantics. âIonization conjectureâ is the strict-binding formulation, with threshold bound states not excluded. âBeyond the square-root exponentâ is 2ĎâĄ(n)2^Ď( n) at inverse-tower rate, not 2n1/2+Îľ2^n^1/2+ for a fixed Îľ>0 >0. 8 Family by family Each card states the claim, describes the extracted instruments and their roles, lists established ingredients, and records caveats. Section and lemma numbers refer to the source papers. The compact status lines report supplied formalizations or the initial extractionâs assessment; they do not report a Lean build performed for this survey. 8.1 Number theory and arithmetic geometry 8.1.1 003 ¡ Zero-free half-plane ReâĄs>7/8Res>7/8 Lean, agent-generated, unreviewed | architecture: combination, leaning new Every Dirichlet L-function and every finite-order Hecke L-function over ââĄ(â3)Q( -3) has no zeros in ReâĄs>7/8Res>7/8. The main paper has 199 pages; a human-edited companion reaches 11/12. Corollaries include Vinogradovâs least-nonresidue conjecture. Extracted instruments. ⢠Embedding the MĂśbius sum in a sextic family. Set Auâ(D)=âÎźâĄ(n)âνâ(n)âĎnâ(u)âWâ(Nân/D)A_u(D)=ÎŁÎź(n)ν(n) _n(u)W(Nn/D) with Ďn _n the sextic symbol. Rows u=p6u=p^6 are near-copies of the target, so a mean-square bound over u controls A1A_1. Poisson in u produces sextic Gauss sums; the HasseâHeath-Brown identity absorbs Îź into cubic Gauss sums, which are Fourier coefficients of the KubotaâPatterson cubic theta function; its transformation law converts the sextic twist into a quadratic one, where GoldmakherâLouvelâs large sieve has no (MâL)2/3(ML)^2/3 loss. The general sextic sieve would only give D7/3D^7/3. The initial search found no earlier use of cubic metaplectic automorphy to bound MĂśbius sums. ⢠Cube completion and transfer. Keeping the full index nâb3nb^3 allows automorphy to be applied. The argument then removes cubes by MĂśbius inversion and iterates with contracted row ranges. The initial extraction classifies this as an incremental development of Heath-Brown 1995 and DunnâRadziwiĹ. ⢠Continuation from a common signal, saturated-witness zero detector, compensated probe (Part I, the push from 11/12 to 7/8). This introduces additional accounting into Littlewoodâs ÎźâÎź zero-free reduction and the Montgomery / MaynardâPratt detector; the initial assessment is incremental. Reused. KubotaâPatterson theta and DunnâRadziwiĹ cusp expansions; GoldmakherâLouvel and BaierâBansal large sieves; Heath-Brownâs recursion; ThornerâZaman prime counting; Hecke functional equation. Caveats. The needed bound is comparable to GRH on average over a family for which the general cubic sieve is sharp. The twist bookkeeping in the theta reflection is therefore a central point to check, as is the dependence of constants on the character. 8.1.2 004 ¡ Hilbertâs tenth problem over âQ not formalized | new architecture | depends on two other OpenAI papers No algorithm decides whether an integer polynomial has a rational zero; the problem has Turing degree 0â˛0 , already for degree â¤4⤠4. The paper explicitly gives no existential definition of â¤Z in âQ and no Diophantine model, so this route does not conflict with Mazurâs conjecture. Extracted instruments. ⢠Finite rational tests with compactness. The construction starts with a recursive theory in which every ring element a carries an elliptic point TaâmâEâ(FR)T_aâ mE(F_R), F=ââĄ(2)F=Q( 2), on a fixed rank-one curve. Adjoin fâĄ(a)=0f(a)=0, Skolemize, and feed finite initial segments of the ground constraints to the âQ-oracle. Dovetail these tests with enumeration of integer tuples: a root ends the enumeration, while failure of a test ends the no-root branch. Each terminating run uses finitely many oracle queries, without a uniform bound. To prove termination, suppose all tests pass; compactness embeds a model in the rational sort of an elementary extension; âelliptic indicesâ Ρ:Râââ¤Îˇ:Râ^*Z are additive and injective; local tests at âcontact primesâ force a~âĄÎˇâĄ(a) aâĄÎˇ(a) to high q-adic precision; a height bound h(A~)âŞfBh( A) _fB against hâĄ(xâĄ(ΡâĄ(aj)âP))â2âh^â(P)âΡâ(aj)2h(x(Ρ(a_j)P))â 2 h(P)Ρ(a_j)^2 gives B2âŞB^2 B, so the indices are ordinary integers and the root is integral. This replaces the Diophantine-definition approach (Poonen, Koenigsmann, MazurâRubin, KoymansâPagano). The initial comparison found no matching architecture. ⢠Five-point height estimate. For the sourceâs fixed five-point set C, fixed exceptional prime set S, and constants H,c>0H,c>0, the bound is hâĄ(s)â¤Hâ MSâ(s)ch(s)⤠H¡ M_S(s)^c for sâ1â(â)âs ^1(Q) . Here h is logarithmic Weil height, and MSM_S is the squarefree product of primes outside S with odd contact order at one of the five fixed branch values of the Shimura curve X=ShâĄ(B210)X=Sh(B_210), genus 5, modulo its AtkinâLehner group. Even contact gives an unramified fiber; a sign-obstruction splitting yields an odd 2-adic representation; modularity, Javanpeykarâs bound, GaudronâRĂŠmond isogeny estimates and Pazukiâs height comparison complete the argument. The statement concerns this specified five-point configuration; no analogue for other branch sets is asserted here. The initial extraction classifies the statement as new and the proof as a combination of established methods. ⢠Pole-parity existential formula. The construction gives ÎŚ with â¤âÎŚ(â)âb:Z (Q) \b: negative valuations are even off a finite set\, via 2-descent on two curves with Monsky matrices and exact Selmer rank 3. This replaces the DemeyerâVan Geel and quaternion predicates and is classified as a new combination. Reused. DPRM; Poonen 2002 index reading; CasselsâTate; Deligne canonical models; DarmonâGranville; GreenâTaoâZiegler with Selberg sieve; compactness. Caveats. The argument depends on two other unverified OpenAI manuscripts: âFontaineâMazur modularity at the prime 2â and âA pointwise 2-converse for elliptic curves with rational two-torsionâ. The second is needed as written to eliminate Sha[2]. The proof of termination uses a non-constructive compactness argument. 8.1.3 017 ¡ Irrationality exponent of Ď is 2 Lean, 867 files, not in catalogue | combination bordering new | logarithm extension requires a separate argument For every ν>2ν>2 and all large q, |Ďâp/q|âĽqâν|Ď-p/q|⼠q^-ν; hence the FlintâHills series converges. The previous bound cited by the initial extraction is 7.103 (ZeilbergerâZudilin 2020). The threshold is ineffective. Extracted instruments. ⢠Separated-weight interpolation (Thm 2.1). Fix integers m,KâĽ1m,K⼠1 and positive rational w0,v0,θw_0,v_0,θ with 0<θ<10<θ<1 and Kâθm<1,Kâw0v0âθm<1.Kθ^m<1, K w_0v_0θ^m<1. Choose positive rational coordinate weights w1,âŚ,wmw_1,âŚ,w_m successively above the sourceâs thresholds; each threshold depends only on the fixed data and previously chosen weights. Put W=(w0,w1,âŚ,wm)W=(w_0,w_1,âŚ,w_m) and V=(v0,w1/θ,âŚ,wm/θ)V=(v_0,w_1/θ,âŚ,w_m/θ). At centers aj=(1,cjâ1,âŚ,cjâm)a_j=(1,c_j1,âŚ,c_jm), 0â¤j<K0⤠j<K, require c0âi,âŚ,cKâ1,ic_0i,âŚ,c_K-1,i to be pairwise distinct for each coordinate i. Polynomials of W-degree at most H then realize all packets of V-weight strictly less than H under the jets Y=1+tY=1+t, Xi=cjâi+ui+logâĄ(1+t)X_i=c_ji+u_i+ (1+t), for all sufficiently large, sufficiently divisible integers H. Divisibility depends only on the weights; the lower threshold for H may depend on the centers. The proof uses a Roth/Dyson-type curve inequality, nefness on a weighted blow-up, ampleness, Serre vanishing and Rees pushdown. Related interpolation mechanisms occur in Masser 1981, Fischler 2005 and FischlerâNakamaye 2014. ⢠Weighted transverse multiplicity (Lemma 2.2) and normal-basis rigidity. A BĂŠzout-type bound determines the normal-basis index set. The proof combines Philipponâs derivative chain with multiplicity estimates. ⢠Two ways to make the determinant small (§3). Rows evaluated at rational approximations to periods, 2âiâjâpi/qi2ijp_i/q_i, are expressed exactly as test rows of the entire functions [ua]âPâ(ez,z+u)[u^a]P(e^z,z+u). The conversion costs qiâνq_i^-ν for each unit of transverse index. Rows with the same index test the same functions, allowing Laurentâs Taylor-degree collision argument to produce a saving that increases with the dimension m. The parameter comparison is feasible exactly when ν>2ν>2. Reused. Laurentâs interpolation determinants; Rothâs separated denominators; Philippon zero estimates; Demaillyâs jets; Mondalâs weighted BĂŠzout; Stacks Project. Caveats. An analogue with centers (rj,jâpi/qi)(r^j,jp_i/q_i) for rââ>0â1r _>0 \1\ is a proposed extension. The claim ÎźâĄ(logâĄr)=2Îź( r)=2 needs a separate proof, including the interpolation hypotheses, rational-height costs and determinant estimates. It is not established by the source comparison in this survey. The initial extraction also flags the interpolation argumentâs nearest prior art as requiring closer comparison. 8.1.4 032 ¡ Rational Hodge conjecture for CM abelian varieties not formalized | combination For every complex CM abelian variety the cycle map onto rational Hodge classes is surjective in every codimension; with Milneâs results this gives the Tate conjecture for abelian varieties over finite fields and the Hodge standard conjecture for abelian varieties in all characteristics. The repository describes this as one of two results produced outside its fixed computation procedure. The withdrawn eightfolds paper is not cited. The other papers in this family use this result as an input, without supplying inputs to its proof. Extracted instruments. ⢠Four-factor switch with algebraic contraction. This reduces every CM Hodge class to one tensor relation v1+v2=v3+v4v_1+v_2=v_3+v_4 among odd sign functions, through chains of two-row swaps composed with ample powers and scalar descent. The paper presents this as incremental over Hazama 2003, AndrĂŠâMilne and GaoâUllmo. ⢠Surface criterion with fixed-input variation of a rank-two theta tensor. On a compact ball quotient of SU(V), V a Hermitian 3-space of signature (2,1), Gaussian-completed Taylor coefficients of theta series give holomorphic one-forms and a (2,0)-form ÎW=âÎ1â§Î2 _W=ÎŁ _1 _2. Freeze the finite theta input and the level, move only the positive-Lagrangian data at the compact place; the period âŤÎžâ§ÎžÂŻâ˛ Ξ Ξ stays nonzero by continuity, and weak approximation lands on a rational endpoint with the other sign pattern. The initial extraction found no precedent for this step; the rest extends KudlaâMillson and BergeronâMillsonâMoeglin. ⢠Degree-one CM extraction: Hecke operators at a split prime satisfy ÎŚ3âD1âÎŚ2+qâD2âÎŚâq3âD3=0 ^3-D_1 ^2+qD_2 -q^3D_3=0 on the Albanese of the full PEL moduli space; the q-adic valuation of the active eigenvalue reads off the CM sign, and weak admissibility converts slope into Hodge type, so one gets rational maps to the prescribed CM abelian varieties without Rogawskiâs endoscopic classification. Reused. Lefschetz (1,1), Galois trace descent, HodgeâRiemann, BorelâHarish-Chandra, Mumford GIT, NĂŠron models, crystalline comparison, Milneâs Hodge-to-Tate theorems, Hazama and Abdulali for the generalized conjecture. Caveats. The source contains about 3,900 lines of unformalized TeX. The Satake normalization, covariance of the constant line and slope formula require consistent sign conventions. The continuity assertion is a central analytic step to check. 8.2 Analysis and geometry 8.2.1 074 ¡ Kakeya maximal conjecture in â3R^3; Kakeya sets in â4R^4 not formalized | combination leaning new (3D) | new framework (4D) The sources claim âKδâfâL3â(S2)â¤CÎľâδâÎľââfâL3\|K_δf\|_L^3(S^2)⤠C_ δ^- \|f\|_L^3 in â3R^3 (the maximal conjecture, stronger than the WangâZahl set conjecture), and every set in â4R^4 containing a unit segment in every direction has Hausdorff dimension 4, without measurability or compactness assumptions. The manuscripts have 97 and 175 pages. The earlier bound cited by the initial extraction in â4R^4 is 3.059. Extracted instruments. ⢠Deformed critical-exponent surface with BV selection. A two-parameter family of critical inequalities balancing a smoothed temporal-deficit cost against a plank-clustering exponent defines hâĄ(p,z)h(p,z), the least admissible exponent; the theorem is hâĄ(p,0)=0h(p,0)=0. If it fails, hâzh-z is coordinatewise monotone, hence locally BV. BV theory gives approximate differentiability almost everywhere. The source then uses coordinatewise monotonicity to sandwich values at an arbitrary nearby point between comparison values in the density-one set, obtaining ordinary total differentiability almost everywhere; at a differentiability point the partials prescribe the deficit and plank shape of âequality sequencesâ, and a minimum-delay argument forces a canonical profile and self-similar âstationary packetsâ. This replaces the sticky/plany/grainy induction on scales of WangâZahl. The initial search found no matching construction in the Kakeya literature; the familiar âextremal configurationâ heuristic is the ancestor. ⢠Two-frame entropy transfer of projection theorems. Four coordinates of a line refine at rates (0,Ď,â,1)(0,Ď, ,1); two marked events give two frames related by an explicit linear map; a robust planar projection lemma (RenâWang Furstenberg in shaded form) plus product-slope pinning shows the product of marginals hits the second frameâs support with probability â¤Î´Îşâ¤Î´^Îş while the true coupling hits with probability 1; data processing gives IâĽÎşâÎśâlogâĄDIâĽÎşÎś D, contradicting a chain-rule bound. The initial comparison found no earlier use of this information bound to apply a projection theorem to dependent events. ⢠Chart/horizon framework with narrowness trichotomy (4D). Lines carry one hidden coordinate; a âchartâ is a box-times-interval where one quadratic test fits well; the âhorizonâ is the infimum time cost of true terminal systems; charts normalize and compose. Three regimes (potential/conservative field with âdegree restorationâ, a Heisenberg-type âhorizontal modelâ, whole-interval localization) each manufacture a cheaper fit, contradicting extremality. This replaces polynomial Wolff axioms: the quality of quadratic fits becomes the variational quantity. Reused. GWZ 2026 convex-clustering estimate (reformulated as a weighted plank lemma, the real dependence of 4D on 3D); RenâWang, WangâWu; multilinear Kakeya; HochmanâShmerkin entropy across scales; OrponenâShmerkin; Christâs quasiextremals; BasuâPollackâRoy. Caveats. The two manuscripts total 272 pages and use nested limits, slow diagonal choices, triangular subsequences and almost-everywhere offsets. Their order of limits needs detailed checking beyond the selected comparisons made here. The three-dimensional argument cites another unformalized OpenAI restriction paper as an alternative route. The initial extraction identifies RiosâSawyer as an uncited antecedent. Literature comparisons remain incomplete. 8.2.2 087 ¡ The Mahler conjectures original inspection: symmetric Lean coverage only; broader solution modules supplied, unbuilt | new identity For origin-symmetric convex bodies KâânK ^n, the source claims |K|â|Kâ|âĽ4n/n!|K||K |⼠4^n/n!, with equality for linear images of Hanner polytopes. For general convex bodies, use the SantalĂł point sâĄ(K)âintâĄKs(K) and define PâĄ(K)=|K|â|(KâsâĄ(K))â|.P(K)=|K|\,|(K-s(K)) |. The general claim is PâĄ(K)âĽ(n+1)n+1/(n!)2P(K)âĽ(n+1)^n+1/(n!)^2, with equality exactly for simplices; for a simplex its SantalĂł point is its centroid. Thus the equality statement for the polar is made after the indicated centering. In the symmetric case sâĄ(K)=0s(K)=0. The third source claims cGâ(intâĄKĂintâĄKâ)=4c_G(intKĂintK )=4 for origin-symmetric KâânK ^n and nâĽ2n⼠2, with embeddings at every capacity strictly below 4. The initial extraction inspected symmetric formalization coverage only. The snapshot also supplies general-Mahler and symmetric-polar solution modules; a sorry in a comparator challenge is a statement placeholder, not evidence that the separate solution module is a stub. None was built here. Extracted instruments. ⢠The conformal lens. FâĄ(z)=8Ď2ââ(â1)jâz2âj+1/(2âj+1)2F(z)= 8Ď^2ÎŁ(-1)^jz^2j+1/(2j+1)^2 maps the disk onto a convex lens whose boundary, under uniform angle, has uniform imaginary coordinate and a fair-sign real coordinate (Lemma 3.1, âlens boundary lawâ). For a strip body A=|biâ X|â¤1A=\|b_i¡ X|⤠1\ form Ί=z:bjâzâD =\z:\ b_jzâ D\. The map is Grossâs 2019 conformal Skorokhod example, as the paper acknowledges. The initial comparison found no earlier application to volume products. The lens replaces the tube domain used by Nazarov and Berndtsson. ⢠Holomorphic mass pushed to the boundary. For a holomorphic map f:ââdââNf:U ^d ^N, NâĽdN⼠d, assume that fâ1â(0)=0f^-1(0)=\0\, its leading homogeneous part has degree kâĽ1k⼠1 and is nonzero away from zero, and every sublevel |f|2â¤s\|f|^2⤠s\, 0<s<10<s<1, is compact in U. The integral of the sum of squared d-by-d Jacobian minors over |f|2<1\|f|^2<1\ is then at least (Ďâk)d/d!(Ď k)^d/d! (the sourceâs special case of Lelong comparison). Apply to fk=(gâ(b1âz)k,âŚ)f_k=(g(b_1z)^k,âŚ) with g=Fâ1g=F^-1, substitute ui=Ďi1/kâeiâθiu_i= _i^1/ke^i _i, let kââkââ: Fatou pushes the mass onto boundary samples, giving S=âIPIâĽ1S= _IP_I⼠1 where PIP_I is the probability that d independent uniform boundary samples solve all strip constraints. The rescaling that turns Lelong mass into feasibility probabilities had no precedent in the literature examined. ⢠Feasible-simplex identity (Prop. 5.1): 1â¤S=d!4dââŤA|ÎŁX|âXâ¤d!4dâ|A|â|Aâ|1⤠S= d!4^d _A| _X|\,dX⤠d!4^d|A||A |, where ÎŁX _X is a union of interior-disjoint simplices convâĄ(0,Îľiâbi)conv(0, _ib_i) over feasible signed bases, with an explicit deficit. Equality forces âlens-cost mediansâ for every triple, then Limaâs criterion and HansenâLima give the Hanner classification. The identity is classified as new in the initial extraction. Reused. Gross 2019; Demailly; CauchyâBinet; Hannerâs formulas; Lima and HansenâLima (the Lean reproves the median-to-Hanner step itself); FradeliziâMeyer; Klartag 2018 for the general case. Caveats. The general-body argument uses about twenty selected decimal constants and SymPy certificates. Its reasoning summary leaves the conclusion dependent on uniform scalar inequalities. The symmetric paper presents a self-contained argument without that qualification. 8.2.3 362 ¡ Relativistic VlasovâMaxwell, 3D, large data Lean, 207 files, continuation step included | combination For the one-species system with no background charge, the source assumes f0âCcâ(âx3Ăâv3),f0âĽ0,E0,B0âCbââ(â3,â3)âŠL2â(â3,â3),ââ E0=Ďf0,ââ B0=0,Ďf0(x)=âŤâ3f0(x,v)dv. gatheredf_0â C_c^â(R_x^3ĂR_v^3), f_0⼠0,\\ E_0,B_0â C_b^â(R^3;R^3)⊠L^2(R^3;R^3),\\ â¡ E_0= _f_0, â¡ B_0=0, _f_0(x)= _R^3f_0(x,v)\,dv. gathered Here every spatial derivative of the fields is bounded, the fields have finite energy, and the nonnegative phase-space datum is smooth and compactly supported. Under these hypotheses the paper claims a unique global classical solution, smooth on each finite time interval and with compact phase-space support there, without a size restriction. The repository supplies a formalization covering a continuation statement; it was not compiled or kernel-checked for this survey. Extracted instruments. ⢠Signed momentum increment bootstrap (Prop. 2.1): for a receiver with energy wâ¤Pw⤠P, |VâĄ(t2)âVâĄ(t1)|â¤MâPât2ât1+AâĄ(t2ât1)âP2âL/w|V(t_2)-V(t_1)|⤠MP t_2-t_1+A(t_2-t_1)P^2L/w, the norm âtaken after integrationâ. With P=2nP=2^n each doubling takes time âĽc/logâĄ2n⼠c/ 2^n; â1/nÎŁ 1/n diverges, so the momentum support stays bounded on every finite interval and the GlasseyâStrauss continuation theorem completes the argument. This replaces pointwise field bounds that lose w w. The time-integrated increment idea is in CheverryâIbrahim 2025; the initial extraction identifies the bootstrap formulation and logarithmic doubling argument as the new features. ⢠Signed force identity along source labels (Lemma 6.1): the LiĂŠnardâWiechert kernel along a sourceâs retarded branch equals a total derivative plus residuals with no source acceleration and no inverse powers of the source deficit, at the cost of a term proportional to the receiverâs own acceleration. The physical ancestor is the HeavisideâFeynman form; the analytic version with moving receiver is new in this setting. ⢠Occupation of retarded bins, direction-change counting, selection (§4, 7, 8): at most CâL6/δCL^6/δ direction changes of size δ; an improved occupation bound in a window; a selection weight with Îľ=10â5 =10^-5 and an exponent contradiction (0.496z versus 0.41z) that makes the receiver coefficient â¤Cwâ1/2⤠Cw^-1/2, cancelling the loss exactly. The occupation estimate adapts Pfaffelmoserâs method to the light cone; the counting and closure are classified as new. Reused. GlasseyâStrauss representation; LukâStrain cone flux; Lazarovici label change; Pallardâs cone Jacobians; Pfaffelmoser; Kirchhoff; GagliardoâNirenberg; Picard. Caveats. The reasoning summary states that the cited continuation theorem alone does not establish the required estimates, whereas the paper presents them as proved. CheverryâIbrahim is cited six times in the summary and omitted from the paper. The exponent comparison has a small margin. A repository formalization is supplied, but no machine check was run for this survey. Uniqueness is asserted only among global classical solutions. 8.2.4 304 ¡ HilbertâSmith conjecture in every dimension not formalized | new Every locally compact second-countable Hausdorff group acting faithfully and jointly continuously on a connected Hausdorff second-countable topological manifold of positive finite dimension without boundary is a Lie group. The equivalent exclusion concerns faithful jointly continuous â¤pZ_p actions on such manifolds, for every prime p. Pardonâs 2013 proof covered dimension 3 via Smith theory and geometrization; the surveyed argument does not use Yangâs theorem, Smith theory, cohomological dimension or cell-like maps. Extracted instruments. ⢠Compact-source test categories TâĄ(X)T(X): the thick subcategory of Dbâ(ShRâ(X))D^b(Sh_R(X)) generated by RâfââRBRf_*R_B for arbitrary continuous maps f from compact polyhedra. Stalks may be infinite-dimensional and images non-constructible, yet Verdier duality restricts with invertible biduality, Rg!=RgâRg_!=Rg_* is duality-preserving for any continuous g, and Verdier quotients have a âgerm descriptionâ via a cutoff lemma. This replaces Woolfâs perfect/constructible Witt groups (whose excision may fail) and RanickiâWeissâs chain-level duality (the exact antecedent of the cutoff). ⢠Fixed sphere lattice / bounded comparison. The semialgebraic-to-continuous comparison Fdâ(Sd)âEdâ(Sd)F_d(S^d)â E_d(S^d) has kernel and cokernel killed by 2ed2^e_d, via BalmerâWalter localization, a dense-doubling map with Κâd=dâΚ=2 d=d =2 (classical exponent-2 bound of HornbostelâSchlichting), and Hardt triviality supplying an integer-valued signature. So Edâ(Sd)ââ=ââuÂŻE_d(S^d) =Q u with image in Ldâ1ââ¤âuÂŻL_d^-1Z u for LdL_d fixed before any action data: âintegral before rationalizationâ. ⢠Character classes and equal parts in a fixed lattice. The orbit sheaf splits into eigensheaves of the â¤pZ_p generator; finite partitions give self-adjoint projectors becoming germ endomorphisms; for m=pkm=p^k faithfulness yields a region over which the orbit map is an m-sheeted trivial cover; a locally constant unit multiplier cyclically permutes the parts as a real isometry; Serreâs odd-sphere degree maps concentrate the class; each part equals (4/pk)âuÂŻ(4/p^k) u, impossible once pk>4âLdp^k>4L_d. The initial search found no earlier version. Reused. Newman 1931 and Pardonâs chart reduction; KashiwaraâSchapira duality; Balmerâs triangular Witt groups; Woolfâs cone lemma; RanickiâWeiss cutoff; Hardt triviality; DranishnikovâFerryâWeinberger telescope; Äech theory and Haar averaging. Caveats. Several steps require closer examination: whether the BalmerâWalter hypotheses pass to localizations of the generated categories; whether RâtâRt_* commutes with the infinite eigensheaf sums used; and whether the restricted pairing is isometric in the germ quotient. The odd stabilization d>nd>n is essential to the argument. 8.3 Combinatorics and theoretical computer science 8.3.1 102 ¡ Unique Games Conjecture Lean, 475 files, full statement, PCP theorem reproved | new gadget For every fixed Îľ,δâ(0,1/2) ,δâ(0,1/2) there is a fixed alphabet 2sF_2^s and a deterministic polynomial-time reduction from 3SAT to bipartite Unique Games with translation constraints, value âĽ1âξ⼠1- on satisfiable and â¤Î´â¤Î´ on unsatisfiable inputs. The formal object fixes alphabet, machine and predicates; Îľ and δ are independent. The development also formalizes a Dinur-style PCP theorem, HĂĽstadâs 3LIN and the KhotâMinzerâSafra Grassmann expansion theorem from scratch. Extracted instruments. ⢠Latent alphabet gadget (Lemma 2.1, §2). The construction consists of a binary space VâK=2âV K=F_2 , a nonlinear map C:VâKC:Vâ K with CâĄ(x+k)=CâĄ(x)+kC(x+k)=C(x)+k, and a rational noise law Îź on V with Pr[C(x+a)â C(x)]â¤pâ [C(x+a)â C(x)]⤠p^* for independent uniform xâVxâ V and aâźÎźa Îź, while every subspace of VâV^* with large restricted rank detects aâźÎźa Îź with probability âĽ1/8⼠1/8, the rank threshold depending only on pâp^*, fixed before â . It is built from the quadratic block QâĄ(x)=(x2âx3,x1âx3,x1âx2)Q(x)=(x_2x_3,x_1x_3,x_1x_2) over 2dF_2^d, update spaces indexed by the q2+q+1q^2+q+1 lines of 3F^3 (the quadratic term cancels on a line), a trace-duality âalignment equationâ zâ gâĄ(z)=z1âz2âz3z¡ g(z)= z_1z_2z_3 characterizing rank loss, recursive concatenation with a harmonic potential bounding rank loss by 4θ per level. The resulting noise rarely changes the honest evaluation (completeness â1â 1) yet forces 0.9 of Fourier mass below bounded rank, so the existing degree-two KMS inverse theorem applies unchanged. BarakâKothariâSteurer 2018 proposed higher-degree tests for exactly this and could not compose them; here degree stays two and the noise changes. The initial search found no matching gadget. ⢠Exact table keys with translation-orbit folding (§3.3): tables are affine maps on homogeneous answer coordinates, keys invariant under sparse projections, vertices are translation orbits, so the sparsely projected prover shares the UG labels âwithout an additional consistency testâ. Combination of KhotâSaket virtual tables and MinzerâZheng. ⢠Row-fiber abundance by erasure (Lemma 4.4): KMS gives one good slice per fiber; re-randomizing the function where good fibers are sparse and a Hoeffding union bound over slice descriptions shows good advice has probability âĽÎˇâ2ââârsâĽÎˇ 2^- r_s independent of k. The initial extraction identifies this as the new step in the advice game; the reasoning summary records âKMS just existence of one fiber, need union randomization argumentâ. Reused. HĂĽstadâs 3LIN gap; KMS Grassmann expansion through BKSâs matrix chart; KhotâSaket folding and list decoding; KMS/DKKMS/MinzerâZheng smooth advice game; DinurâSteurer parallel repetition twice; SchwartzâZippel. Not used: Majority is Stablest, high-dimensional expanders, sum-of-squares. Caveats. The argument does not use other OpenAI manuscripts as inputs. Its reduction exponent and alphabet size are tower-like in 1/pâ1/p^*, which accounts for compatibility with the AroraâBarakâSteurer subexponential algorithm, although the paper does not discuss this point. The reasoning summary records that UGC arose as a subgoal of a different prompt about the basic SDP threshold. 8.3.2 107 ¡ Matrix multiplication exponent Ďâ¤9/4Ď⤠9/4 Lean, straight-line definition of Ď over âC | new as a proof of an Ď bound ĎâĄ(â)â¤9/4Ď(C)⤠9/4, compared with the previous bound 2.371177 cited by the initial extraction. The 13-page argument is non-constructive: it bounds every point of Strassenâs asymptotic spectrum and gives âno competitive finite matrix sizeâ. Extracted instruments. ⢠Finite separation of a shared leg and the shared-leg entropy inequality (Prop. 3.1, Cor. 3.2). Starting with A=âhAhA= _hA_h and a shared X-leg, the construction takes L=5âML=5M copies and substitutes roots of unity. The resulting r-sum is a DFT that retains the terms satisfying uâv+2â(gâh)=0u-v+2(g-h)=0. On these terms, the degeneration weights g2,hâuâh2,âhâvg^2,\ hu-h^2,\ -hv add to (gâh)2(g-h)^2, so the weight-0 component is the complete direct sum â¨hAhâBXâ(M) _hA_h B_X(M). For nonzero tensors TiT_i sharing the first space and occupying matched, pairwise disjoint sectors on the other two legs, every spectral point Îť and probability vector q satisfy ÎťâĄ(T)âĽepXâHâ(q)ââÎťâ(Ti)qiÎť(T)⼠e^p_XH(q)Î Îť(T_i)^q_i, where T=âiTiT= _iT_i and H(q)=ââiqilogqiH(q)=- _iq_i q_i. The construction retains all blocks at a factor-5 cost; SalemâSpencer hashing and laser-method zeroing-out retain at most one block per shared variable. Its ingredients are the CohnâUmans DFT, Strassen degeneration, and the method of types. The initial literature comparison identified no matching combination. ⢠Spectral growth on polynomial multiplication. CâĄ(a,b)=âxiâyjâzi+jC(a,b)=ÎŁ x_iy_jz_i+j has rank a+bâ1a+b-1; symmetrize over S3S_3 to a profile PâĄ(a,b)â¤(a+bâ1)1/tP(a,b)â¤(a+b-1)^1/t. Two degenerations fed into the inequality (a ClebschâGordan filtration giving discrete concavity in b, and a three-window partition giving tripling) force PâĄ(a,a)âĽa4/3P(a,a)⼠a^4/3, hence 3âtâ¤9/43t⤠9/4. Strassen duality converts the uniform spectral bound into an asymptotic-rank bound. The source compares its spectral argument with barriers for specified tensor-extraction methods, including the laser and universal methods. Its proof constructs no degeneration into matrix products; this comparison does not establish that it evades every possible barrier. AlmanâLiâs 2026 âStrassen calculusâ is the uncited template, used there only for cwqcw_q-type bounds. ⢠Detecting characters (App. A): a fixed-point (SchauderâTychonoff) proof of the needed case of Strassenâs spectral theorem. The initial extraction classifies this reproof as incremental. Reused. Bini interpolation; Strassenâs asymptotic spectrum; combinatorial degeneration; method of types; ClebschâGordan exact sequence. Caveats. The stated theorem concerns âC. The argument bounds spectral profiles through a specified collection of inequalities; a better exponent would require a further argument. No Lean build was performed for this survey. 8.3.3 157 ¡ Counterexample to Hadwigerâs conjecture Lean, 276 files, no explicit graph | new The source constructs arbitrarily large m-vertex graphs with independence number â¤2⤠2 and connected-matching number <m/100<m/100, where every pair of matching edges must have an edge between their endpoint sets. The resulting Hadwiger number is hâĄ(G)<26âm/75+2/3h(G)<26m/75+2/3, hence hâĄ(G)<0.347âmh(G)<0.347m for sufficiently large m, while ĎâĽĎfâĽm/2Ď⼠_f⼠m/2. This would also refute the ReedâSeymour fractional weakening and the FĂźrediâGyĂĄrfĂĄsâSimonyi connected-matching conjecture. Parameters: g=109+1g=10^9+1, m=21000â gâ M0â nm=2^1000¡ g¡ M_0¡ n; the Lean extracts m from an eventually-true filter statement. Extracted instruments. ⢠The hole relation with tensor certification (§2). Vertices are random injective frame maps over 2F_2 with prescribed self-Gram; two vertices have a âholeâ iff witnesses Îťi _i, Îťj _j in a cut-profile space satisfy a shared-tensor equation and gradient identities ujâUi=râĄ(Îťi)u_jU_i=r( _i), uiâUj=râĄ(Îťj)u_iU_j=r( _j) with râĄ(x)=a+TâĄ(x,â )r(x)=a+T(x,¡), T symmetric bilinear, and aâĄ(Îťi)+aâĄ(Îťj)=1a( _i)+a( _j)=1. Summing the gradient identities around a hypothetical triangle cancels all bilinear terms and leaves 0=10=1, so holes are triangle-free deterministically and Îąâ¤2ι⤠2 follows directly. This replaces the pseudorandom triangle-free graphs of prior Îą=2Îą=2 attacks. The initial comparison found no matching construction. ⢠Entropy-minimizing container argument (§3): KleitmanâWinston fingerprinting on the conflict graph of units whose progress measure is the minimum relative entropy of a law obeying marginal caps; each recording raises the minimum by âlogâĄ(1âÎľ)- (1- ); when no feasible law remains, a FordâFulkerson cut certifies the residual is covered by small sets. It transfers a distributional supersaturation theorem (âany capped unit law has four-cross-hole probability âĽ2â100âgâN⼠2^-100gNâ) to the random sample. The initial search found no precedent for this potential or the terminal min-cut certificate. ⢠Scalar recipe / gradient realization / collision machine (§4â13): witnesses as sums of â¤7⤠7 atoms, keys forcing all four holes from O(n) scalar Gram bits, overlap forced by min-entropy peeling, Walsh bounds, a FriezeâKannan âtwisted cut normâ increment, and a characteristic-2 Boolean flat-extension lemma. This is an extensive collection of problem-specific constructions; the initial extraction did not settle its novelty. Reused. PlummerâStiebitzâToft Îąâ¤2ι⤠2 reduction; Cambieâs connected-matching-to-minor count; KleitmanâWinston; CsiszĂĄr; FordâFulkerson; weak regularity; LaurentâMourrain flat extension. Caveats. The argument gives neither an explicit graph nor an explicit clique-minor number. Many subsequence/compactness steps are non-quantitative by design (âNo exponential rate uniform over all stages is assertedâ). IllingworthâSteinerâs separate result of 28 September 2026 disproves the dominating variant [10], which requires a stronger kind of clique-minor model. A counterexample to that variant need not violate Hadwigerâs conjecture itself. Both constructions use graphs with Îąâ¤2ι⤠2. The repository supplies a Lean development for the claim surveyed here, but it was not compiled for this survey. 8.3.4 158 ¡ The plane is not 5-colorable Lean, unrestricted statement, â24,500â 24,500 lines | new Every 5-coloring of â2R^2 with arbitrary color classes has a monochromatic unit pair, so the chromatic number of the plane is 6 or 7, in ZFC. The formal statement is literally ÂŹââĄc:ââFinâ 5 â\,c:C \,5 proper. The proof uses neither a SAT solver nor a vertex list; its argument is structural and ergodic. Extracted instruments. ⢠Transfer of colorability via Haar rigidity of wild character laws (§2â4). Let E be the algebraic plane, K its algebraic unit circle, D the dual of E with discrete topology, CâDCâ D the continuous characters. A K-invariant probability on D is âwildâ if it gives C measure zero. The stated theorem is that every wild K-invariant probability is Haar. Its proof combines a FurstenbergâZimmer compact tower with an explicit approximation property, a transfinite relative-singularity lemma, conditional multiple averages with van der Corput, a radial difference inequality wâĄ(|AâB|)â¤wâĄ(A)+wâĄ(B)w(|A-B|)⤠w(A)+w(B), and a number-field general-position lemma. To obtain the coloring consequence, Følner-average any proper coloring over EâKE K; the spectral âwildâ part of each color indicator is uncorrelated at all algebraic translations and can be discarded, leaving a measurable âweakâ coloring with almost no monochromatic unit pairs. Thus a proper k-coloring exists if and only if a weak measurable k-coloring exists, for every k. The literature since Falconer treats measurable and unrestricted chromatic numbers as possibly different; the claimed transfer equates existence in these two formulations. The initial literature comparison found no matching transfer theorem. ⢠Angular palettes, binary centers, transition graph (§5â6): weak-â* limits of circle samples around a center; a 60â exclusion; the bound âat most two colors per direction a.e.â proved by an expanding-action bounded-distortion argument on six circle maps. Combination of Falconer/Townsend/SokolovâVoronov density mechanics with a new dynamical separation. ⢠Common exclusion continua (§7): threshold and renormalize indicators into a continuous map to the 1-skeleton of the 4-simplex; a Brouwer cover obstruction forces a non-null loop; midpoint preimages become continua that each exclude two colors in a crescent. Combination. Reused. de BruijnâErdĹs; Falconer, Payne; FurstenbergâZimmer; Bochner/SNAG; Følner means; Fourier decay of the circle; Brouwer; Hatcher covering theory; Moser spindle with a rational placement certificate. Caveats. The rigidity theorem is dense and relies on a transfinite induction; the initial extraction places it inside the Lean closure (Rigidity.lean). The inspected comparator configuration disables the optional nanoda independent kernel recheck; no build was run here. The paper never exhibits a finite 6-chromatic graph, consistent with the method. A footnote disputes a pseudonymous manuscript; that dispute is not assessed here. 8.3.5 159 ¡ ErdĹsâs reciprocal-sum conjecture original label: companion only; repository also links a headline development, unbuilt | new architecture The source claims rkâ(N)â¤CkâNâexpâĄ(âckâ(logâĄN)Îľk)r_k(N)⤠C_kN (-c_k( N) _k) for each fixed kâĽ3k⼠3, with ck,Îľk>0c_k, _k>0, and hence progressions of every finite length in any set with divergent reciprocal sum. The dyadic deduction is valid: for a k-progression-free set A, ânâAâŠ[2j,2j+1)1nâ¤2âjrk(2j+1)âŞkexp(âckâ˛jÎľk), _nâ AâŠ[2^j,2^j+1) 1n⤠2^-jr_k(2^j+1) _k (-c _kj _k), and the last expression is summable in j. By contrast, âmâĽ2expâĄ(â(logâĄm)c) _m⼠2 (-( m)^c) diverges for 0<câ¤10<c⤠1 and converges for c>1c>1. The original discussion of the weaker LengâSahâSawhney log-log bound must be understood in the former range; divergence is not true for every positive c. The 198-page source uses the LSS inverse theorem as an external input. Extracted instruments. ⢠Triangular polynomial cells with descending precision budgets. A density-increment region is a nested system âbhâChâ(u,b<h)âlhâââ¤wh\|b_h-C_h(u,b_<h)-l_h\|_â⤠w_h, h=1,âŚ,Dh=1,âŚ,D, where integer blocks of weight h are determined exactly, ChC_h is a weighted-degree polynomial with unbounded coefficients, and Qh=logâĄ(2/wh)Q_h= (2/w_h) is the precision. The key inequality is that the loss at weight i, Qiâ˛âQiQ_i -Q_i, is bounded by a polynomial in the precisions at weights above i, never in QiQ_i itself. With D fixed, descending induction keeps all precisions polynomial in p=logâĄ(1/Îą)p= (1/Îą) over O(p) increments, which is exactly a quasipolynomial bound. This replaces increments that reset to a sub-progression and lose a power each round. The trace shows it emerging in Part I as the fix for a compounding-resources recurrence. The initial search found no earlier use of this terminology or architecture. ⢠Shift comparison and positive counting: a one-sided structure theorem at higher nilsequence degree (degree 1 is KelleyâMeka sifting plus SchoenâSisask), with a two-kernel trick converting a deficit into a surplus detectable by upper bounds. The initial comparison identified binary-system and corners analogues, and classified the stated higher-degree propagation as new. ⢠Relative lifting with additive rank and exact marked projection: sample integer-affine paths inside a cell, recover an ambient nilsequence from local ones, keep every old integer slot exact; returned rank independent of ambient dimension. This is a quantitative local-to-global transfer, classified as a new formulation; its correctness was not established for this survey. Reused. LSS inverse theorem; SchoenâSisask almost-periodicity; KelleyâMeka sifting; GreenâTao polynomial orbits; Lengâs equidistribution; CandelaâSisask densification; CRT prime boxes. Caveats. The quantitative upper bound was not verified here. The repository documentation links a development for the reciprocal-sum consequence, beyond the lower-bound companion noted in the initial extraction; that development was not built here. The paper claims an improvement from log log to log for every k at once. The traceâs Part I never closed (âcircularity concern unresolvedâ) and Part I ends in âclaimed/assertedâ. The argument has a long chain of dependencies. An appendix extends LSS to product groups of dimension (2+p)A(2+p)^A with a step-drop lemma uniform in parameter count, which the model itself flagged as delicate. 8.4 Algebra and operator algebras 8.4.1 196 ¡ Counterexample to Kaplanskyâs zero-divisor conjecture Lean, 124 files, includes finite 2-dim K(G,1) | combination; separator step new The source constructs a finitely presented torsion-free group with a finite two-dimensional classifying complex and nonzero Îą, β in 2â[G]F_2[G] with Îąâβ=0ιβ=0. The construction is non-constructive: 8258 generators, a random graph on nâłe300000n e^300000 vertices. The initial extraction cites 2026 revisions by Mineyev and Shin that describe the conjecture as open. Extracted instruments. ⢠Odd cross-intersection parity mechanism. The alphabet consists of the 16513 points of PG(2,128) plus three letters; each vertex of two graphs gets an outgoing label set whose ordinary part is a projective line, arranged so every pair of label sets across the two graphs meets in an odd number of points. Cone off components; Îą and β are sums of root-component path labels. Stepping both coordinates by a common letter leaves the product element invariant, every vertex of the product graph has odd degree, so every component has even size and every coefficient of Îąâβιβ vanishes mod 2, âindependently of how edges will be matchedâ. This relaxes Mineyevâs even-product matching and the RipsâSegev non-unique-product requirement to âodd-degree product graphâ realized by an oddtown-style design. ⢠Bounded-pattern estimate for a girth-conditioned random-matching model with prescribed types (Prop. 3.1): conditional on girth at least L, the probability that such a system exists is oâĄ(1)o(1) as the admissible graph size tends to infinity: it has at most K positive-length paths, total length Lâ¤Hâ¤CâL⤠H⤠CL, at most I interval pairs, and at most ÎľâH H unpaired occurrences. All paths are cyclically immersed and closed, except possibly one immersed interval starting at a prescribed root. Paired occurrence intervals are disjoint, obey the signed-label matching rules, and traverse distinct underlying undirected edges. The constant Îľ is fixed before K,C,IK,C,I, which remain fixed in the limit. The proof proceeds via multiplicity stages, ânearly aligned blocksâ from a simultaneous Dirichlet choice, and a transfer-matrix bound. This reverses the GromovâOllivierâOsajda model (fixed graph, random labels) into fixed label types, random graph, with no small-cancellation hypothesis. ⢠Planar-separator extraction plus cone-picture band surgery (Props. 4.4, 5.1): any reduced spherical arrangement is cut by LiptonâTarjan recursion to bounded clusters that the estimate excludes; the surgery along bands joining two occurrences of a lifted edge proves asphericity and root protection together. The initial extraction classifies the separator step as new in this setting and the surgery as incremental over Gruber and Bereznyuk. Reused. Graphical presentations; projective-plane incidence parity; configuration model with switchings; Ollivierâs density counting; LiptonâTarjan; Brownâs periodic-resolution argument. Caveats. The result concerns characteristic two and does not provide a concrete presentation. The source explicitly addresses quantifier order and the dependence introduced by conditioning. Its Lean development was not compiled here. A separate direct-finiteness manuscript dated 4 October adapts this machinery and is not formalized. 8.4.2 197 ¡ Counterexample to Kaplanskyâs direct-finiteness conjecture Lean, 125 files, search certified at hâ¤217h⤠217 | new criterion The construction gives a finite field of characteristic two, a finitely presented group G with odd torsion, and a, b in K[G] with aâb=1,bâaâ 1ab=1,\ baâ 1. Such a group would be non-sofic by ElekâSzabĂł, and the construction would also contradict Gottschalkâs surjunctivity conjecture. Extracted instruments. ⢠The incidence criterion (Thm 3.1): let â be an odd prime and K a finite field of characteristic two containing a primitive â root of unity. Take a finite hypergraph with t points and nonempty blocks, every point on exactly â+1 +1 blocks, and bipartite incidence graph of girth at least 12, together with vectors xvâKmx_vâ K^m with âvâfxvâxv=0 _vâ fx_vx_v T=0 per block and âvxvâxv=âIm _vx_vx_v T=-I_m, with 0<m<tâ¤mââ20<m<t⤠m ^2; these data yield the counterexample. The key identity uses the fact that â+1 +1 is the number of lines through the origin of â2F_ ^2, so local copies of â2F_ ^2 glue along the blocks, and âuâKvu=1+âfâv(âuâLfuâ1) _uâ K_vu=1+ _f v( _uâ L_fu-1) turns the two identities into UâT=ImUT=I_m after averaging. This gives a local-to-global certificate for failure of direct finiteness; the closest relative is DykemaâHeisterâJuschenkoâs universal left-invertible-element groups, which encode cancellation patterns but give no such criterion. ⢠Polynomial pairing on a punctured affine space (Prop. 2.3): Newton interpolation polynomials for a set of holes give the vectors; products of degree â¤qâ2⤠q-2 sum to zero on every full line by the power-sum identity, and removing the holes leaves âI-I. The multiplication property also appears in GolowichâLin and DinurâLiuâZhang codes, which the paper acknowledges; it does not invoke a theorem from those constructions. ⢠Hole trades with random slabs and the local lemma (§5): replacing the fan of lines through a hole by parallel lines in a plane preserves every other pointâs degree; Linnikâs theorem supplies ââĄâ1modq100 âĄ-1 q^100 so bundles of q directions exist; short incidence cycles are enumerated and excluded by the LovĂĄsz local lemma. The resulting regular high-girth line system is classified as a new construction. ⢠Character-twisted HNN packing and the sandwich certificate (§4): Ďv _v conjugates KvK_v onto a reference copy while twisting by a linear form, so t coordinates share m slots with orthogonal character idempotents; J0âÎâC=eâĄ(TâUâP)J_0 C=e(TU-P) lives in the smaller algebra K[H], where the homomorphism âevery group element âŚ1 1, zâŚÎśz Îśâ gives XâXâItâ 0X TX-I_tâ 0 by rank. The planar Euler-characteristic embedding argument uses a form of small cancellation; the DykemaâJuschenko finite-group step is classical and made explicit. Reused. ElekâSzabĂł for non-soficity; DykemaâJuschenko reduction; HNN embedding; Newton interpolation; LovĂĄsz local lemma; Linnik via Xylouris. Caveats. The construction was not executed at the prescribed scale (q up to 22172^217, dimension âĽ1200⼠1200); the certificate is algebraic. The Lean statement does not include non-soficity. The repository supplies a formalization for the odd-characteristic companion, but not for the torsion-free companion dated 4 October. 8.4.3 248 ¡ Thompsonâs group F is not amenable Lean, conceptual, F defined from scratch | new use, leaning new F admits no positive normalized left-invariant mean, settling Geogheganâs 1979 question in five pages. The formal statement defines F as dyadic piecewise-linear homeomorphisms and the invariant mean on âââ(F) ^â(F); it gives no finite certificate, and the constants are existential. Extracted instruments. ⢠Recursive Hilbert-ball-valued coloring of dyadic partitions. For a dyadic partition T of [0,1][0,1], define pâĄ(T)=fâĄ(1DââjpâĄ(TIj))p(T)=f ( 1D _jp(T_I_j) ) when T respects D fixed internal basic dyadic intervals with strictly positive pairwise gaps, and define it to be 0 otherwise. Here TIjT_I_j is the normalized restriction. The recursion is well founded because restriction decreases the number of cells. Applied to the image partitions gâT(n)gT^(n), it produces colors XIâ(g)X_I(g) for which the parent color equals f applied to the mean of the descendant colors. Mooreâs 2013 reformulation uses finite, nonrecursive tree colorings. The initial comparison found no earlier version of this recursive rule with a fixed-point-free f. ⢠BenyaminiâSternfeld displacement map as an amenability obstruction. Let f be an L-Lipschitz self-map of a Hilbert unit ball with âfâĄ(x)âxââĽÎ´>0\|f(x)-x\|âĽÎ´>0 everywhere (BenyaminiâSternfeld 1983; the source constructs δ=1/2δ=1/2 on L2â([0,1],â2)L^2([0,1];R^2)). For each g in the nonempty finite averaging set AâFAâ F, the recursive identities give the pointwise estimate δ2â¤âmâĄ(g)âfâĄ(mâĄ(g))â2â¤L2Dââi=1Dâziâ(g)âmâĄ(g)â2.δ^2â¤\|m(g)-f(m(g))\|^2⤠L^2D _i=1^D\|z_i(g)-m(g)\|^2. The correlation comparisons control the finite averages, not each summand pointwise. With AE_A denoting uniform averaging over gâAgâ A and Ρ the maximum normalized translation defect for the selected transports, δ2 δ^2 â¤L2Dââi=1DAââziâmâ2 ⤠L^2D _i=1^DE_A\|z_i-m\|^2 â¤L2â(4D+4â(1â1D)âΡ). ⤠L^2 ( 4D+4 (1- 1D )Ρ ). Choosing D>4âL2/δ2D>4L^2/δ^2 gives a positive lower bound on Ρ, contradicting the Følner criterion. The map is non-affine and F does not act on it; the initial extraction found no earlier use of this displacement theorem for this amenability problem. ⢠Correlation comparison via pair transport: for internal basic dyadic intervals I<JI<J and Iâ˛<Jâ˛I <J in (0,1)(0,1), where I<JI<J means maxâĄI<minâĄJ I< J, an element of F carries I affinely onto Iâ˛I and J affinely onto Jâ˛J . The positive gaps and internal endpoints are part of the hypothesis. This compares averaged color correlations for the strictly separated pairs in the construction; it makes no such assertion for nested pairs or arbitrary boundary-touching intervals. Reused. Følnerâs criterion (formalized forward direction); CannonâFloydâParry partition model; BenyaminiâSternfeld; convexity of the square norm. Caveats. The five-page argument addresses Geogheganâs amenability question. The pointwise and averaged estimates above were compared with the source; this check does not certify the full proof. A direct invariant-mean argument can fail because a fixed partition level may have measure zero. The source instead chooses a finite averaging set A first and selects the level afterwards. Other OpenAI preprints are used only for corollaries. 8.4.4 287 ¡ All free group factors are isomorphic Lean, 77 modules, in docs but not catalogue | combination | proves more than it states LâĄ(n)â LâĄ(n+1)L(F_n) L(F_n+1) for nâĽ3n⼠3 by exhibiting a freely generating Haar n-tuple inside LâĄ(n+1)L(F_n+1); LâĄ(2)â LâĄ(3)L(F_2) L(F_3) via Dykemaâs amplification at t=2t= 2; RÄdulescuâs dichotomy then makes all interpolated free group factors LâĄ(r)L(F_r), 1<râ¤â1<râ¤â, isomorphic with fundamental group â>0R_>0. One consequence is that free entropy dimensions would not be generator invariants. The claim differs from expectations recorded in the initial extraction; Popa 2024 and SchafhauserâTikuisisâWhite 2025 list the problem as open. Extracted instruments. ⢠Small cocycle with a prescribed word value (Lemma 4.1). Let Î=n =F_n, and place the coefficient h on the first generator only. The Fox cocycle of wm=(ab1)(ab2)âŻ(abm)aw_m=(ab_1)(ab_2)¡s(ab_m)a, where bj=x2jâx3âx2âjb_j=x_2^jx_3x_2^-j, is TmâhT_mh with Tm=1+âÎťâĄ(pj)T_m=1+ÎŁÎť(p_j) and freely generating pjp_j. Since TmâTmâ/mT_mT_m^*/m converges to free Poisson(1), which has no atom at 0, a cutoff inverse supplies h with âĽhâĽ2â¤(dm)â1/2\|h\|_2â¤(dm)^-1/2 before finite-support approximation, where d>0d>0 is a fixed spectral cutoff, and small âTmâhâδeâ2\|T_mh- _e\|_2. The spectral cutoff controls the discarded mass; the absence of an atom at zero does not supply a uniformly bounded inverse. The associated flow changes each generator by OâĄ(âhâ)O(\|h\|) while changing the long word by a full unitary factor. Fox calculus and the free Poisson law are classical; the initial extraction identified their use to obtain this displacement as the new feature. The repositoryâs Lean development uses a combinatorial partial inverse and also treats n=2n=2, beyond the paperâs argument. ⢠Trace-preserving polynomial flow driven by conjugates of a bounded logarithm (Prop. 3.1): S=argâĄCS= C, ODE Ajâ˛=iâĄ(âghjâ(g)âAgâSâAgâ)âAjA_j =i( _gh_j(g)A_gSA_g^*)A_j; trace preservation via a universal initial trace identity on a formal algebra; displacement bounds via a three-block free-Khintchine inequality. A specialization of Voiculescuâs cyclomorphy to Haar unitaries with relations; incremental. The new choice is the fixed bounded logarithm and that the flow fixes C, so a Nielsen move converts the wordâs displacement into absorption of the extra generator. ⢠Adaptive error budgets and L2L^2-density âWâ W^*-generation (§5): The current-stage estimate treats the newly produced word as one unitary slot. After substitution, the word-polynomial Lipschitz constant does depend on word length: LâĄ(F)=âν|cν|â|vν|L(F)= _ν|c_ν|\,|v_ν| for F=âνcνâvνF= _νc_νv_ν. Future error budgets are chosen after that constant is known; norm convergence preserves the Haar law. Incremental; Shlyakhtenkoâs Fuchsian preprint of 10 Sep 2026 (âobtained using ChatGPT Proâ) already uses finite automorphisms fixing one element plus limiting generation, and the Lean uses Baire instead. Reused. Voiculescuâs free probability; Fox calculus; RicardâXu Khintchine; cyclomorphy as a model; Nielsen moves; Dykema amplification and RÄdulescu dichotomy (the Lean avoids both and proves LâĄ(3)â LâĄ(â)L(F_3) L(F_â) directly). Caveats. The claimed result would refute the ConnesâShlyakhtenko L2L^2-Betti conjecture for LâĄ(n)L(F_n); this consequence is not discussed in the source. A broader free-product absorption statement would require separate hypotheses and is not asserted here. The reasoning summary identifies trace preservation and limiting generation as dependencies. 9 Family by family, second group The second group belongs to the initial extraction and uses the same entry format. An entry marked âno fresh searchâ was compared with directly retrieved primary sources but did not receive a separate literature search. 9.1 Number theory and arithmetic geometry 9.1.1 002 ¡ Full BSD formula from low Selmer corank not formalized | new construction | three-paper chain plus an unpublished preprint If the q-power Selmer group of E/âE/Q has corank 0 or 1 at some prime q, then rank equals analytic rank equals that corank, Sha is finite, and the exact BSD leading-term formula holds with no hypotheses on reduction, torsion, isogenies, CM or residual image. The main paperâs own contribution is the exact valuation at every odd prime; rank and finiteness come from the companion âSelmer converseâ, the 2-adic part from the âtwo-primaryâ companion, and the auxiliary quadratic fields from family 006, which rests on Smithâs 2025 preprint. Extracted instruments. ⢠Tame variables, finite models and residual concentration (§3â4). The coefficient ring is â¤pâ[[t,u1,âŚ,um]]Z_p[[t,u_1,âŚ,u_m]] where t is the cyclotomic or anticyclotomic variable and each uju_j is a nonprincipal-ultrafilter limit of cyclic p-power characters at auxiliary primes râ1râ 1 p-adically. NekovĂĄĹ-style Selmer complexes are replaced by bounded finite free cochain models whose matrices have ultrafilter limits, keeping cup products, duality and homotopies. âResidual concentrationâ adjoins tame directions until one-sided determinants are nonzero mod (p,t), using a first-order lift test with Chebotarev-chosen commutators. This is where Eisenstein and small-image primes are absorbed. This extends TaylorâWilesâKisin auxiliary primes and ScholzeâManning ultrapatching; the combination (ultralimits of tame characters as formal Iwasawa variables, later specialized to zero) had no precedent in the literature examined. ⢠Integral character-division test and codimension-two divisor removal (Lemma 3.9, §9): Weierstrass division in a distinguished tame coordinate makes an analytic-over-algebraic quotient integral; any divisor would force a Selmer jump along a codimension-one locus, excluded by adjoining directions until simultaneous jumps have codimension âĽ2⼠2. This replaces main-conjecture input by divisibility plus divisor avoidance. Combination. ⢠Theta implication with a retained nilpotent tame parameter (companion §4â9, main §7â8): a holomorphic theta family on U(3,1) at both real places of ââĄ(DâDâ˛)Q( D ) whose constant FourierâJacobi term is a toric period specializing via BDPâs inverse differential operator to a truncated series over kâĄ[t]/(tb)k[t]/(t^b); cusp lifting mod pnp^n, base change to GL4GL_4, BellaĂŻcheâChenevier extension extraction giving Artin length âĽb⼠b against a first-order upper bound â¤2⤠2. This replaces SkinnerâUrban and CastellaâLiuâWan Eisenstein congruences, with no ordinarity of E. New as a construction. Reused. GrossâZagier and Kolyvagin; Katoâs zeta elements; Kolyvagin derivatives with MazurâRubin switches; BDP measures; Cassels and Milne isogeny invariance; BurungaleâFlach for CM rank 0; ChaiâHida rigidity; PoitouâTate. Caveats. Proposition 5.14 asserts Katoâs divisibility at every odd prime including Eisenstein primes, stronger than the statements found in the initial comparison, and is a principal step to check. The foundational steps require attention (ultrafilter limits of cochains, âno lim1lim^1 termâ). The companionâs appendix cites an undated 185-page author-hosted draft, apparently not load-bearing. 9.1.2 007 ¡ Ordinary two-point Chowla repository reports Lean coverage; comparator and solution coverage not independently checked here | combination bordering new For fixed integers a1,a2âĽ1a_1,a_2⼠1 and b1,b2âĽ0b_1,b_2⼠0 satisfying a1âb2âa2âb1â 0a_1b_2-a_2b_1â 0, the source claims |â1â¤nâ¤XÎťâĄ(a1ân+b1)âÎťâ(a2ân+b2)|â¤Ca1,a2,b1,b2âX(logâĄX)c(XâĽ3). | _1⤠n⤠XÎť(a_1n+b_1)Îť(a_2n+b_2) |⤠C_a_1,a_2,b_1,b_2 X( X)^c (X⼠3). The exponent c>0c>0 is absolute; the implied constant can depend on the fixed forms, and no uniformity for coefficients growing with X is asserted. The corrected binary Elliott conclusion is qualitative, under uniform non-pretentiousness of an original factor and the same conditions on the affine forms. The initial extraction describes ordinary two-point Chowla as open before this release. The exponent is not given numerically. Extracted instruments. ⢠Terminal-scale divisor bins with padding anti-concentration. Dilation nâŚqâdân qdn changes the scale, which explains the role of dilation-invariant logarithmic averaging in the earlier approaches of Tao, HelfgottâRadziwiĹ and Pilatte. Here divisor pairs are confined to bins jâΡâ¤logâĄ(dâq)<(j+1)âΡjΡ⤠(dq)<(j+1)Ρ so the full-divisibility term is F(X)+O(Ρ) at a fixed scale; d is a product of J primes from disjoint supplies, q a squarefree âpaddingâ weighted 4ĎâĄ(q)4^Ď(q); a characteristic-function anti-concentration lemma spreads divisor mass so each bin costs (C/W)Jâ¤eâJ=(logâĄX)âc(C/ W)^J⤠e^-J=( X)^-c. This replaces dilation invariance of logarithmic weights. The fixed-scale bin plus mass-spreading padding is not in HelfgottâRadziwiĹ, Pilatte or TaoâTeräväinen. ⢠Finite residue comparison via Bravermanâs theorem. Prime sets have joint period far exceeding X, so CRT cannot compare interval averages with the independent-residue model. Each residue is encoded as the first L15L^15 bits of a jittered quotient, equality tests become DNFs, the bit law is made exactly t-wise uniform by the AlonâGoldreichâMansour Fourier trick, and Bravermanâs theorem (polylog independence fools AC0AC^0) gives error eâL10e^-L^10 for every event in the proof, all written as bounded-depth circuits. This replaces Pilatteâs rank-truncated sieve. The initial extraction found no earlier arithmetic application of Bravermanâs theorem. ⢠Degree-normalized two-band divisor graph with matched centering (Part I): a core band weighted e2âÎşe^2Îş per prime and a center band with factor 1p|xâθ/p1_p|x-θ/p, θ=1/4θ=1/4 chosen so that lit and unlit residues cancel to OâĄ(pâ2)O(p^-2) before absolute values; edges divided by the originâs total divisor weight. Combination over HelfgottâRadziwiĹ and Pilatteâs graphs. Reused. HelfgottâRadziwiĹ divisibility graph and prohibited paths; Pilatteâs composite labels and non-backtracking operator; MatomäkiâRadziwiĹâTao short sums (corrected 2022 version); GranvilleâSoundararajan distance; Brun truncation. Caveats. The reasoning summary makes the conclusion conditional on simultaneous-witness elimination, forest counting, finite-residue comparison and spectral-transfer bounds, while the paper states these steps as proved. They are the main points identified for further checking. Part I gives no rate. 9.1.3 010 ¡ FontaineâMazur modularity at the prime 2 not formalized | combination | input to Hilbertâs tenth Every continuous irreducible representation r:GââGL2â(âÂŻ2)r:G_Q _2( Q_2) that is odd (detrâĄ(c)=â1 r(c)=-1 for complex conjugation c), unramified outside finitely many primes, and de Rham at 2 with two distinct HodgeâTate weights is a Tate twist of the 2-adic Galois representation attached to a classical cuspidal eigenform, âincluding all residual representationsâ: scalar, reducible, dihedral. The earlier results cited by the initial extraction covered p=2p=2 only for irreducible non-solvable and nearly-ordinary solvable residual images. Family 004 rests on this paper alone (not on its two satellites). Extracted instruments. ⢠Marked lines and transverse charts (§5â6). After a solvable totally real base change through abelian 2-extensions with 2 split and a bounded number of bad primes, record an invariant ordinary line only at the m=[F:A]m=[F:A] dyadic places over one place of A, with m/dâ0m/dâ 0. Restricting to points where marked lines are transverse to every global invariant line forces the local residual representation to be scalar at marks and makes the extension cocycle vanish there, so the reducible locus has dimension below the connectedness dimension (SGA2) of the chart and the residual fiber is connected. This replaces SkinnerâWiles and Panâs ordinary covering, which records a line at all p-adic places. The proposed new step is to mark a vanishing fraction of places to obtain connectedness, while leaving the propagation step unrestricted at 2. ⢠Finite-jet ultrapatching at a characteristic-two curve (§4): TaylorâWiles patching at a one-dimensional prime with residue field k((t)), enhanced coefficient ring carried through all rings, ultraproducts of jets, a uniform ArtinâRees bound; full support obtained on the tame âΡ = iâ model and transferred to the unipotent âΡ = 1â model via the common special fibre (KhareâWintenbergerâs characteristic-2 form of Ihara avoidance). Incremental over Pan 2022 §4; new only in the jet bookkeeping that survives a non-finite residue field. ⢠Ordinary character family with Thorne points and a polynomial-orbit lemma (§7): for locally reducible targets, an ordinary family finite dominant over weight space whose dense weight-0,1\0,1\ points are modular by Thorneâs Theorem D; a direct Banach-representation lemma shows a unit-eigenvector fixed by the unipotent radical is locally algebraic âwithout assuming that algebraic vectors commute with specializationâ. Combination; the seed set is entirely dependent on Thorne. Reused. Chenevier determinants; Wang-Erickson algebraization; BĂśckleâIyengarâPaĹĄkĹŤnas local geometry; PaĹĄkĹŤnasâTung blocks; ColmezâDospinescuâPaĹĄkĹŤnas; BreuilâEmerton; NewtonâThorne adjoint Selmer vanishing; BillereyâMenares lifts; JacquetâLanglands and cyclic base change; Ramakrishna switching. Caveats. The principal external input is Thorneâs August 2026 preprint [6]; without that input, the stated argument for locally reducible targets, and the Hilbertâs-tenth reduction that uses it, would require a replacement. Tabaâ 2020 (unrefereed) is cited for normality of completed tensor products. The pro-modularity satellite is doubly dependent. The paper consistently attributes each device to Pan, KhareâWintenberger, SkinnerâWiles, BIP and Thorne; the new mathematics is combination and p=2p=2 bookkeeping. The initial extraction completed fresh searches and reports checking the statements of each essential citation against its primary source. 9.1.4 040 ¡ Blochâs conjecture for surfaces with pg=0p_g=0 not formalized | new strategy For every smooth connected projective complex surface with pg=q=0p_g=q=0, degree is an isomorphism CâH0â(S)ââ¤CH_0(S) with integral coefficients; hence the full Bloch conjecture for pg=0p_g=0 (general type forces q=0q=0, Îş<2Îş<2 is BlochâKasâLieberman). For pg=0p_g=0, the stated motivic consequences concern the rational Chow motive hâ(S)âh(S)_Q: Kimura-finiteness and vanishing of its transcendental degree-two summand. The pure-Tate conclusions for hâ(S)âh(S)_Q, powers SmS^m and Hilbert schemes S[n]S^[n] additionally require q=0q=0. The integral zero-cycle statement does not imply an integral Tate-motive decomposition. Two unrefereed competing preprints (Guletskii, Banerjee) are cited as âproposed proofsâ with no logical dependence. Extracted instruments. ⢠Marked Chow relation from Quot-scheme localization (Thm chow-relation). On the Quot scheme of rank-0 quotients of L1âL2L_1 L_2 with fixed determinant, mG_m acts with weights Âą1Âą 1. The class ÎâĄ(t)=qââ(hpâcâh2â(Q)(1)âcâh2â(Q)(2)âŠ[B]vâiârĂ[XĂX]) (t)=q_*(h^p\,ch_2(Q)_(1)ch_2(Q)_(2)âŠ[B]^virĂ[XĂ X]) has equivariant codimension p+4âvp+4-v; if v>p+2v>p+2 its codimension-2 part would carry a negative power of t, impossible for a non-localized class, so it vanishes. GraberâPandharipande localization rewrites the same class as a sum over fixed loci |T|Ă|H|ĂX[n1]ĂX[n2]|T|Ă|H|Ă X^[n_1]Ă X^[n_2], yielding âWCW=0 _WC_W=0 in CâH2â(XĂX)âCH^2(XĂ X)_Q with each CW=cWâ[ÎX]+C_W=c_W[ _X]+ external products. This supplies BlochâSrinivas decompositions needing no family, covering or automorphism. Positive-dimensional localization relations are standard (FaberâPandharipande; MarianâOpreaâPandharipande used this exact setup for Lehnâs conjecture); the initial search found no earlier use of this approach for Blochâs conjecture. ⢠Chow universality with two output factors retained and the universal diagonal coefficient: run the EllingsrudâGĂśttscheâLehn recursion in Chow without integrating two marked copies of X; components containing both outputs give a scalar times [ÎX][ _X], computed by a formal rule depending only on âŤc2 c_2 and intersection numbers, hence transportable between surfaces with equal numerics âwhether or not T, H are effectiveâ. The initial assessment is a new combination, with related work by MaulikâNeguĹŁ and NeguĹŁâOberdieckâYin. ⢠Auxiliary-surface comparison via the divisor cosection (K2=9K^2=9): on the CartwrightâSteger surface (pg=q=1p_g=q=1, same Chern numbers as a fake projective plane), ChangâKiemâs cosection eliminates every divisor component except the empty divisor and the unique canonical divisor, pairing with Re Ď gives coâuât=sâcmâiâdc_out=s\,c_mid, a length-2 blow-up computation gives cmâiâd=12c_mid=12, so c=12â(s+Ď)>0c=12(s+Ď)>0, bypassing a length-20 Hilbert-scheme integral. The construction distinguishes pgp_g exactly through whether |K||K| is empty or a point. New as a strategy. Reused. BlochâSrinivas; Roitman torsion; GraberâPandharipande; MOP/OpreaâPandharipande Quot obstruction theories; EGL recursion; CarlssonâOkounkov; ToĂŤnâVaquiĂŠ and SchĂźrgâToĂŤnâVezzosi derived moduli; KiemâLi cosection; Serreâs classification of indefinite unimodular lattices for K2â¤8K^2⤠8. Caveats. The diagonal coefficient is a formal choice in a non-unique decomposition; detection is legitimate only because the test class is orthogonal to every divisor appearing, which the paper checks. Derived-geometric foundations (fixed obstruction theory, Manolache compatibility) are asserted in a few pages each. No fresh literature search was completed for two of the instrument comparisons. 9.1.5 193 ¡ Serreâs positivity conjecture not formalized | new device For a commutative Noetherian regular local ring R of dimension d and nonzero finitely generated R-modules M,NM,N with âRâ(MâRN)<â _R(M _RN)<â and dimRM+dimRN=d _RM+ _RN=d, the source claims ĎRâ(M,N)=âi=0d(â1)iââRâ(ToriRâ(M,N))>0Ď^R(M,N)= _i=0^d(-1)^i _R(Tor_i^R(M,N))>0, without a restriction on characteristic or ramification. The previously open case was ramified mixed characteristic VâĄ[[x]]/(pâf)V[[x]]/(p-f), pâ2pâ m^2, which BhattâHochsterâMa still called âthe most tantalizing problem that remainsâ. Load-bearing external inputs (CaiâLeeâMaâSchwedeâTucker perfectoidization results, LandâTamme cdh descent for truncating invariants, Maâs Frobenius vanishing) were compared with their arXiv statements in the initial extraction. Extracted instruments. ⢠Supported rational descent (Thm 3.1): let A be a commutative Noetherian â¤(p)Z_(p)-algebra of finite Krull dimension, JâAJâ A an ideal containing p, and H a connective associative A-algebra with central A-action. Let T be a finite commutative A-algebra with a finite group G acting over A, such that SpecâĄTâSpecâĄASpecT is surjective and G is transitive on each geometric fiber. The claimed equivalence is KJâ(H)ââ(KJâ(HâAT)â)hâGK^J(H)_Q (K^J(H _A^LT)_Q)^hG. In the proof, the fiber of rationalized K-theory under inverting p is truncating because Goodwillieâs HN terms cancel, hence a cdh sheaf; finite-flat descent by rational transfers; flattening by blow-up; a âgeometric orbit argumentâ computes invariants. Combination: Voevodskyâs h-topology and SuslinâVoevodskyâs pseudo-Galois covering lemma (uncited) transported to spectrum-valued truncating invariants with noncommutative coefficients. ⢠Rank quotient and supported asymptotic complexes (§4): fix snââs_nââ and an ultrafilter; the perfect hull of sequences (San)(S^a_n), an=OâĄ(sn)a_n=O(s_n), with arbitrary matrix sequences as morphisms, modulo the thick subcategory of oâĄ(sn)o(s_n) sequences. Homology functors land in Serre quotients by null-ultralimit normalized length, giving nonnegative Betti numbers and Euler maps; a Drinfeld dg quotient exhibits the category as Perf of a connective algebra so instrument 1 applies. This turns the sequence of truncated minimal resolutions of finite approximations to the perfectoid parameter quotient into one K-theory class. New as a device; relatives are BhattâHochsterâMaâs lim CohenâMacaulay sequences, Schoutensâs ultraproducts, ChuangâLazarev rank functions. ⢠Two norm comparisons instead of invariance of individual evaluations: ordinary and normalized perfectoid Euler characteristics are compared only after summing over Galois conjugates; both equal râĎAr _A on classes pulled back from the regular base, and descent says invariant rational classes come from A. âNo invariance of Îť under G is asserted or needed.â This is the idea that bypasses non-functoriality of perfectoidization. Combination. Reused. Serreâs reduction to prime pairs via Roberts and GilletâSoulĂŠ vanishing; CohenâGabber normalization; Faltings normalized length; CLMST perfectoidization in mixed characteristic and perfection plus Monsky and Roberts in characteristic p; BhattâHochsterâMaâs âonly H0H_0 survivesâ mechanism via a Koszul-polynomial trick. Caveats. The argument relies on several results from 2022â2026. Further checking should focus on the Verdier-quotient identification âPerfâĄ(H) (H) and its base change, spectral sequences on idempotent summands that need not lift to chain maps, and the interaction between ultralimits and ordinary limits. A December 2025 AI-generated note had already asserted the prime-quotient form; the paper treats it as a claim rather than an established theorem. The initial extraction retrieved primary sources directly but did not complete fresh searches for this family. 9.2 Analysis, dynamics and mathematical physics 9.2.1 143 ¡ Hilbertâs sixteenth problem, uniform bounds not formalized (companion only) | combination For each degree d there is a finite B(d) bounding the number of limit cycles of every real planar polynomial vector field of degree â¤d⤠d: the uniform-boundedness assertion in the second part of Hilbertâs sixteenth problem. The bound is ineffective; ĂcalleâIlyashenko individual finiteness is not used as a premise. The manuscript has 160 pages. The companion concerns the classical LiĂŠnard system xË=yâFâĄ(x) x=y-F(x), yË=âx y=-x, with degâĄFâ¤5 F⤠5; it claims at most two isolated periodic orbits. The repository supplies a formalization of this self-contained companion. Extracted instruments. ⢠Packets on saturated logarithmic flags and the separation theorem (Defs 2.1, 3.1, Thm 3.2): a flag Z1âŤâŻâŤZmâŤ1Z_1 ⌠Z_m 1 of scales with exact triangular log relations; a packet is an analytic function plus two lateral trees of successive expansions in eâaâZje^-aZ_j on nested complex bands with transition estimates and antiholomorphic sources where determinations are glued; if all paired terminal coefficient germs vanish the function is identically zero, by weighted PhragmĂŠnâLindelĂśf and Cauchy corrections. This is a multiscale, parametric, two-determination reorganization of Ilyashenkoâs superexact series and functional cochains, with âdifferentiated closureâ and âretestabilityâ added. Combination. ⢠Absolute isolated-zero finiteness and projection count (Def 11.1, Thms 5.4, 11.2): an open analytic system with margins and its finite differential-algebraic closure has finitely many isolated real solutions when all coordinates including parameters are unknowns; with row rank this gives a uniform bound on fiber components (proper barrier, one generic tilt, Lagrange critical-point induction). Along an escaping sequence of isolated zeros, build a flag, eliminate with a deferred floor, apply separation, perturb a free scale to produce a non-isolated solution. This converts sequence-dependent finiteness into a coefficient-uniform bound. Incremental for the projection principle (Khovanskii 1984, Gabrielov); a new combination in its connection with packet quasianalyticity. ⢠Finite passage templates and matching systems (Thms 9.5, 11.3): LionâRolin preparation of the slope field with all coefficients as parameters, in Euler clocks, puts every cell in an exact monomial normal form; Khovanskiiâs planar Rolle bounds boundary crossings so every cycle is a bounded word in a finite alphabet, matched end to end in finitely many analytic systems; hyperbolicity gives full rank and one component per cycle. This bypasses desingularization, polycycle classification and parameter compactness. Combination; the organizing idea of parametric preparation as a substitute for blow-up was not found elsewhere. Reused. LionâRolin and Opris preparation; BierstoneâMilman and Gabrielov uniform finiteness; Khovanskiiâs Rolle; Gevrey truncation; IlyashenkoâYakovenko cyclic systems; rotated vector fields to make cycles hyperbolic. Caveats. The paper cites Yeung 2025 for a gap in Ilyashenko 1991 at a differential-closure step and claims to repair it through differentiated implicit calculus. That assertion and Sections 6â8, which devote 80 pages to checking packet hypotheses for four transfer models, merit detailed examination. Degenerate singularities and polycycles are not named outside the introduction. The literature comparison was limited. 9.2.2 263 ¡ The ionization conjecture headline not formalized; companions yes | new The source uses the nonrelativistic fermionic Coulomb Hamiltonian on ânL2â(â3,â2) ^nL^2(R^3;C^2), with two electron spin states and kinetic term âÎ/2- /2. The MâĽ1M⼠1 fixed nuclei have distinct positions RjR_j and real charges zjâĽ1z_j⼠1; Z=âj=1MzjZ= _j=1^Mz_j is total nuclear charge. The systemâs net charge in electron-charge units is ZânZ-n, and excess electron number is nâZn-Z. Nuclear repulsion is omitted as a constant independent of n. For the ground-energy infima EnE_n (with E0=0E_0=0), strict binding En<Enâ1E_n<E_n-1 is claimed to imply nâ¤Z+CâMn⤠Z+CM, with universal C; threshold bound states are not excluded. For a neutral atom with one nucleus at the origin and integer ZâĽ1Z⼠1, let ĎΨZ _ _Z be the spin-summed density of any normalized ground state, of total mass Z. Its outer half-electron radius is RâĄ(ΨZ)=infrâĽ0:âŤ|x|>rĎΨZâ(x)âxâ¤12.R( _Z)= \r⼠0: _|x|>r _ _Z(x)\,dx⤠12 \. The stated bounds are 0<câ¤RâĄ(ΨZ)â¤C0<c⤠R( _Z)⤠C and 0<câ¤I1â(Z):=EZâ(Zâ1)âEZâ(Z)â¤C0<c⤠I_1(Z):=E_Z(Z-1)-E_Z(Z)⤠C, uniformly in such Z. The radius retains a fixed exterior mass, not a fixed fraction of all electrons. The initial extraction lists repository formalizations for two ThomasâFermi asymptotic companions (607 and 428 files), not an independently checked proof of the main strict-binding assertion. Extracted instruments. ⢠Noisy-observation conditioning with a dimension-free tilt cost (Lemmas 5.1â5.2). Observe every electron position with independent smooth noise of width âj=rj1.01 _j=r_j^1.01 at dyadic scales, forget labels, obtaining decreasing Ď-fields. For a normalized eigenstate Ψ and an observation event AââąjA _j of probability p>0p>0, put pAâ(x)=PrâĄ(AâŁx)p_A(x)= (A x). With the stated noise law and âhâĽjâhâ2â¤Câââjâ2 _h⼠j _h^-2⤠C_ _j^-2, the vector ΨA=pA/pâΨ _A= p_A/p\, is antisymmetric, in the form domain, has the conditional law, and qâĄ[ΨA]â¤eΨ+Cââjâ2âlog5âĄ(e/p)q[ _A]⤠e_ +C _j^-2 ^5(e/p), with no factor of n or of the number of arrays. The proof uses a score bound, Rademacher symmetrization and the eigenstate multiplier identity. Any failure of a local ThomasâFermi comparison becomes a legitimate low-energy state. This replaces the deterministic HartreeâFock density unavailable for correlated states. The initial comparison found no matching construction in the examined work of Lieb, LSST, FeffermanâSeco, S, Solovej, Nam or Lewin. ⢠Conditional density determines the field (Lemmas 3.4â3.6, 5.3, Prop 10.1): a spatial cut leaves an antisymmetric conditional core with exact energy identity; coherent-state Bernoulli-occupied Slater trials (upper) and per-configuration Neumann bracketing through the empirical fine density of removed electrons (lower) share the same ThomasâFermi constant; two posterior laws are compared via separate tower identities (âno equality of posterior laws is usedâ). Combination. ⢠Outward propagation by convexity-preserved subsolutions under observation forgetting (Lemma 5.4, Prop 11.2): subsolution fields with reaction 4âĎâkât+3/24Ď kt_+^3/2; Jensen for convex f and the tower identity preserve the inequality as observations are forgotten, errors paid by a density with summable expectation. The construction applies Solovejâs multiscale approach to a martingale of conditional fields. Combination. Reused. Liebâs 1984 bound; Zhislin binding; IMS localization; Lewinâs sector localization; LiebâThirring; LiebâSimon Neumann bracketing and ThomasâFermi theory; Solovejâs coherent states and exterior screened-potential strategy; BĂŠnilanâBrezis. Caveats. The argument has many quantitative parameters (L=106L=10^6, exponents 1.01, probabilities r25r^25, r40r^40); the full bookkeeping was not checked. The formalization catalogue marks âPartial progressâ, review âuncheckedâ, and omits the radii development from its results list. The literature comparison was limited. 9.2.3 265 ¡ Two-dimensional area law from a global gap not formalized | new Let Î be a finite induced square-lattice graph, with local dimension qâĽ1q⼠1, and let H=âXhXH= _Xh_X have one Hermitian term per nonempty support X, with âhXââ¤J\|h_X\|⤠J and support diameter at most R in the graph distance of Î . Assume a unique ground state and a full-system gap Î>0 >0. The source claims SâĄ(A)â¤CâĄ(q,R,J,Î)â|âÎA|S(A)⤠C(q,R,J, )| _ A| for every AâÎA , where âÎA _ A is the set of lattice edges crossing from A to its complement within Î . No gap on restrictions, frustration-freeness or translation invariance is assumed. For the open LĂLĂ L square grid with bounded on-site and nearest-neighbor interactions, a companion gives a normalized PEPS approximation with vector error at most Lâ1L^-1 and bond dimension at most CâLcCL^c, with C,cC,c depending on q,J,Îq,J, . The constant is existential. Earlier proofs cited in the initial extraction (AnshuâAradâGosset 2022) need frustration-freeness. Extracted instruments. ⢠Optimized nested positive filters with stationarity and Schmidt pinning (§3). Maximize âĽLmâŻL1ΊâĽ\|L_m¡s L_1 \| over positive filters on nested regions with constraints TrâLj2/aj=1TrL_j^2/a_j=1 and harmonic weights; stationarity forces each filter to commute with the filtered marginal, so filters are clipped marginal powers; a cosh estimate bounds excitation energy, and the global gap converts this into an entropy sum (via a tilt by Ďâu/2Ď^-u/2 and the three-lines theorem). The opposite bound pins a Schmidt vector in trial filters with analytic continuation. Subtracting gives a conditional-entropy discount and a subvolume exponent with no local gap. This replaces the AGSP subvolume argument and is classified as new in the initial extraction. ⢠Replica metric transport (§5â8): on Symkâ(V)Sym^k(V), central operators WQâeâtâFQW_Qâ e^-tF_Q with Schur labels âkâ k¡S(Q), equal on complementary regions; band metrics combined through finite trees of KuboâAndo geometric means as a small subsystem switches sides. The estimates are ââplogN2âĽkaâ¨I(x:F|P)âŠâ- _p N^2⼠k\,a\, I(x:F|P) -err, and energy â¤2âE0+Câa2â (split probability)⤠2E_0+Ca^2¡(split probability), so the displayed information term is linear in a, while the additional energy cost is quadratic in a and linear in the split probability; a slow scan through a collar leaves sublinear mutual information. This replaces Chebyshev/AGSP Schmidt-rank bookkeeping. In the literature examined, encoding conditional mutual information as the derivative of a log-norm comparable to energy had no precedent. ⢠Positive replacement, randomized scanner, amplification (§4, 9, 10): absolute values of Kitaevâs filtered terms retain the gap with exponential tails; random schedules make each interaction rarely split; Poisson-clock products give a local unitary witnessing decoupling. The initial extraction classifies this as a new combination; taking absolute values is an elementary but essential step. Reused. LiebâRobinson bounds; Kitaev filter; AlickiâFannesâWinter; strong subadditivity; SchurâWeyl; de Finetti; KuboâAndo means; Schatten interpolation; random-order chain rule. Caveats. The exponent estimates have a small margin (Îľ=10â5 =10^-5, 0.999952 versus 0.99999), and the replica errors must be controlled uniformly over all histories. The argument gives no quantitative Î -dependence. Not every instrument received a fresh literature search. 9.2.4 268 ¡ The spin-one Haldane gap not formalized; computer-assisted | new criterion For the pure spin-1 Heisenberg antiferromagnet on even periodic rings, the source claims a unique ground state for all even LâĽ60L⼠60 and a uniform gap: ÎłL>4105âlogâĄ8079>4.79Ă10â4 _L> 4105 8079>4.79Ă 10^-4 for LâĽ60L⼠60 and >3.8Ă10â3>3.8Ă 10^-3 for LâĽ2304L⼠2304, versus the numerical 0.4105. Odd rings are not covered. A companion discharges Tasakiâs Assumption 2 for boundary-field chains. Haldaneâs 1983 conjecture for the actual Heisenberg chain had no rigorous proof; the chain is not frustration-free, so the usual AKLT and frustration-free finite-size criteria do not directly establish this claim. Extracted instruments. ⢠Coupled purity bootstrap (Prop 4.4). Two purities of one partition function Znâ(b)Z_n(b) are the Gibbs purity TâĄ(n,b)=Znâ(2âb)/Znâ(b)2T(n,b)=Z_n(2b)/Z_n(b)^2 and the spatial purity SâĄ(n,b)=Z2ânâ(b)/Znâ(b)2S(n,b)=Z_2n(b)/Z_n(b)^2, formed from the spatial-transfer eigenvalues. If a probability vector has purity P, its normalized square has purity Pâ˛P satisfying 1âPâ˛â¤(1âP)22âP2.1-P ⤠(1-P)^22P^2. This gives quadratic improvement in a high-purity regime, not convergence to purity one from arbitrary initial data (a uniform probability vector is unchanged). Squaring Gibbs weights doubles b; squaring spatial weights doubles n. The exact coupling identities remain SâĄ(n,2âb)=Sâ(n,b)2âTâ(2ân,b)Tâ(n,b)2,TâĄ(4ân,b)=Tâ(2ân,b)2âSâ(2ân,2âb)Sâ(2ân,b)2.S(n,2b)= S(n,b)^2T(2n,b)T(n,b)^2, T(4n,b)= T(2n,b)^2S(2n,2b)S(2n,b)^2. The sourceâs quantitative bootstrap assumes even n0âĽ4n_0⼠4, b0>0b_0>0, 0<u0<1/60<u_0<1/6, and constants C,rC,r such that G(u0)â¤C,r=Cu0<1,C(1â3u0)>3,GâĄ(u)=12â((1âu)â1+(1âu)â2+(1âu)â3)2,S(n0,b0)âĽ1âu0,T(2n0,b0)âĽ1âu0. gatheredG(u_0)⤠C, r=Cu_0<1, C(1-3u_0)>3,\\ G(u)= 12 ((1-u)^-1+(1-u)^-2+(1-u)^-3 )^2,\\ S(n_0,b_0)⼠1-u_0, T(2n_0,b_0)⼠1-u_0. gathered Together with the transfer representation, these hypotheses give dyadic defect decay and interpolation to intermediate even lengths. The inequality TâĄ(L,b)>1/2T(L,b)>1/2 alone forces ground-state uniqueness: two ground states would have equal maximal Gibbs weights. The uniform gap ÎłL>logâĄ(1/r)/b0 _L> (1/r)/b_0 uses the quantitative decay and temperature bounds as well. The criterion uses no local ground-state projections; its novelty judgment concerns this gap mechanism, not the elementary purity identity alone. ⢠Self-adjoint spatial transfer operator on bond histories (Prop 3.1): the AizenmanâNachtergaele Poisson expansion regrouped by bond gives a real symmetric HilbertâSchmidt kernel; twisted traces split the spectrum into multiplicity sectors. This gives a rigorous continuous-time quantum transfer matrix in the tradition of Suzuki and KlĂźmper. Combination. ⢠Moment-to-spectrum extraction with exact-integer certificates: partition functions of â¤12⤠12 sites enclosed by floor-Horner in big integers; polynomial filters and capped masses convert moments into spectral bounds; an SU(2)-structured periodic MPS certifies the energy density. The initial extraction classifies this computational method as incremental. Reused. AizenmanâNachtergaele 1994; Suzukiâs quantum transfer matrix; FannesâNachtergaeleâWerner MPS; FoxâGlynn truncation; Tasakiâs 2025 index theorem (companion). Caveats. The argument uses 27 thermal cases and 2 MPS contractions. The verifier was not run for this survey. Self-adjointness requires the real Cartesian decomposition, which restricts the scope of the criterion. 9.3 Combinatorics, geometry and complexity 9.3.1 103 ¡ L=RL=BPLL=RL=BPL Lean, multi-tape Turing-machine statement | new Deterministic logspace equals randomized logspace, one- and two-sided error. The comparator states exactly L=RLâ§RL=BPLL=RL =BPL for a multi-tape model with fresh coins per step and polynomial halting on every coin tape. The record stood at Hozaâs log3/2âĄn/logâĄlogâĄn ^3/2n/ n. The formalization has a narrower scope than the full construction: the effective compiler and numerical bounds are not formalized, and Lean identifiers are obfuscated, which limits the textual inspection reported here to the statement. Extracted instruments. ⢠Exact correction and copy hierarchy (§4). From the nilpotent substochastic transition S on the configuration graph, p0=(IâS)â1âep_0=(I-S)^-1e. A stage applies a correction E with IâD=(I+E)â(IâC)I-D=(I+E)(I-C), moving transition mass into the reward; E is a Lipschitz cutoff iterated a constant number of times (a âfactorial truncationâ lemma); âdetectorsâ set column multipliers to suppress correction on overloaded columns; a copy step splits large entries among copies with an intertwining that transports rewards. Each stage cuts the max entry by 2H2^H while at most doubling active vertices; after O(log n) stages all entries are small. This replaces repeated squaring (SaksâZhou), Richardson iteration and PRG-fooled branching programs. Shortcutting and vertex splitting have precedents; the initial comparison found no matching hierarchy with this doubling bound. ⢠Rank channels and conditional averaging in a shared environment (§3, 5): all randomness is O(log n) bits (a few matrices over PF_P plus salts); retention of a vertex at nested rates via an h0h_0-wise-independent polynomial sampler; averaging over a hash slice without storing identifiers by a lazy walk on the slice via the affine action of SâLHâ(â¤)ââ¤HSL_H(Z) ^H, with Shalomâs explicit Kazhdan constants giving a spectral gap uniform in moduli and âvalidated walk variantsâ guessing the wrap vector. Combination: MargulisâGabberâGalil lifted to H dimensions; new is the conditional sampler on hash slices. ⢠Allowance/clock controller with catalytic key equality (§7â11): telescoping multilevel estimates with longer walks at larger slack; rows stored as exceptions to a default; SchwartzâZippel fingerprints; contour traversal of a program tree charged so the stack telescopes to O(B); a shared B-bit catalytic vector lets equality of two keys be XOR-accumulated in four excursions with O(1) local state; errors measured by a root-Lipschitz loss so relative errors compose. Combination; the catalytic-equality gadget is a candidate new component. Reused. Nilpotent inverse of the configuration graph; k-wise independent hashing; relative property (T) expanders (Shalom, Kassabov); RieszâThorin; CarterâWegman fingerprints; CookâMcKenzie traversal; LangeâMcKenzieâTapp reversibility; catalytic computation (BCKLS). Caveats. The source contains about 400 KB of text and an eight-step chain of sufficiently large constants. It avoids storing a seed hierarchy, the source of the log3/2 ^3/2 space bound in the comparison made by the initial extraction. 9.3.2 112 ¡ Depth-three circuits beyond the square root Lean, 179 files | new The source gives a fixed language in P such that for every real constant A>0A>0, ÎŁ3 _3 circuits (unbounded fan-in, no bottom fan-in restriction, size = gate count) computing its n-bit slice need more than 2Aân2^A n gates for large n: the explicit 2ĎâĄ(n)2^Ď( n) problem of HĂĽstadâJuknaâPudlĂĄk 1995 and Gurumukhani et al. 2024, record 21.282ân2^1.282 n (PaturiâPudlĂĄkâSaksâZane 2005). The growth rate is an inverse tower in log n; this is weaker than 2n1/2+Îľ2^n^1/2+ , as the paper says. Extracted instruments. ⢠Restriction bound independent of clause count (Lemma 3.1). A width-k CNF H under a p-random restriction has the expansion H|Ď=K+Kââj(â1)jââpathsâvih/âaUhH|_Ď=K+K _j(-1)^j _pathsÎ v_i_h/Î a_U_h. Here K conjoins the initially easy clauses (â¤b⤠b live variables), each path records successive hard clauses, and the denominators count violated easy clauses. A marker-mixture identity expresses each path term as a nonnegative weight times the expectation of a width-b CNF: randomly order clauses and markers, then retain the clauses preceding the first marker. The resulting correlation estimate is |EâĄ[Gâ H|Ď]|â¤Wâ corrbâ(G)|E[G¡ H|_Ď]|⤠W¡corr_b(G) with EâĄ[W]â¤1/(1âθ)E[W]⤠1/(1-θ). The Poisson-type tail θ is << 1 for any constant pk when b ⍠pk. Classical HĂĽstad switching has a useful decay estimate when pâk<1/5pk<1/5; the scale pâ1/kpâ 1/k with kâlogâĄSkâ S leads to the n n exponent. In the signed expansion, normalization averages over eligible violated clause indices and cancels their count. The initial extraction classifies this mechanism as new. Talâs L1L^1 switching lemma and small-restriction switching lemmas have different conclusions. ⢠Sparse partition (Lemma 4.1). Every width-b CNF on m variables is a pointwise sum of â¤2Îľâm⤠2 m pairwise disjoint width-b CNFs, each with Cb,ÎľâmC_b, m clauses, for fixed integer bâĽ1b⼠1 and Îľ>0 >0. This follows by combining ImpagliazzoâPaturiâZane sparsification with the disjointness construction of DellâHusfeldtâMarxâTaslamanâWahlĂŠn. The source describes this component as incremental. ⢠Slice language (Def 5.1). The input contains data x, Toeplitz hash bits, a monic polynomial, and t field elements. Acceptance requires the degree-zero coefficient of the polynomial evaluated at the hash to vanish in the quotient-ring representation. In the proof, an irreducible modulus is selected and the hash is required to be injective on the restricted data cube. Random independent field coefficients then give t-wise independent signs on that cube. Averaging subsequently fixes one setting of all non-data bits with a small failure probability over restrictions; a fixed deterministic slice is not itself a random t-wise independent family. The construction combines Krawczyk hashing, AlonâBabaiâItai limited independence, and the evaluator approach of PaturiâSaksâZane. On the good random restrictions with m surviving data bits, its correlation with every width-b CNF is at most 2âm/82^-m/8; the exponent 1/81/8 is independent of fixed b, while the sufficiently large length threshold may depend on b. Parity lacks this property, so the argument is consistent with the tight parity bound. Reused. HĂĽstad-style restrictions and wide-clause truncation; Razborovâs reverse encoding; sunflower lemma; universal hashing; t-th moment bounds. Caveats. The argument does not depend on other OpenAI manuscripts. The mathematical review checked selected identities in Lemma 3.1 and the arithmetic in §6. A separate literature comparison for the marker-mixture device remains incomplete. 9.3.3 156 ¡ Borsukâs conjecture fails in dimension 9 Lean, 275 files, exact real arithmetic | combination leaning new The set X of rank-one projectors uâu T, |u|=1|u|=1, in the trace-one affine hyperplane of Sym4â(â)Sym_4(R), which is isometric to â9R^9 under the Frobenius metric, has diameter 2 2 and cannot be covered by ten sets of smaller diameter, so bâĄ(X)âĽ11>10b(X)⼠11>10; by adjoining points, Borsuk fails for all dâĽ9d⼠9. The previous range cited by the initial extraction was dâĽ64d⼠64 (JenrichâBrouwer). The witness is a compact copy of ââP3RP^3, not a finite set; no finite 9-dimensional counterexample follows. Extracted instruments. ⢠Odd spectral extension of an admissible map. From a smooth partition of unity f on ââP3RP^3 whose positive supports are disjoint for orthogonal lines, define HâĄ(v)=|v|2âfâ([v])H(v)=|v|^2f([v]), EâĄ(Q)=kââŤHâĄ(Q1/2âu)âÎźâ(u)E(Q)=k H(Q^1/2u)\,dÎź(u) on PSD matrices, and FâĄ(A)=EâĄ(A+)âEâĄ(Aâ)F(A)=E(A^+)-E(A^-); F is odd with âFâĄ(A)â1=trâ|A|\|F(A)\|_1=tr|A|, so it is an odd map between spheres and BorsukâUlam gives mâĽNkm⼠N_k immediately, exactly tight. This test map supports the rest of the argument and replaces FranklâWilson and strongly-regular-graph counting. Combination; Kalaiâs survey names the set but asks no topological question about it; AdamsâBushâFrick 2021 is the nearest relative. ⢠Equality-case degree analysis. At m=Nkm=N_k the map has odd mod-2 degree; a maximal support with fewer than k labels gives a positive-dimensional level set inside one affine chart, where the extension descends to LĂââPhâ1âââPaâ1LĂRP^h-1 ^a-1 with vanishing StiefelâWhitney power, degree 0, contradiction. So every facet has exactly k labels and the facets form an 2F_2 cycle. This converts a tight BorsukâUlam bound into rigid combinatorics. New as a technique for Borsukâs problem, as far as could be checked (no dedicated literature search was completed). The Lean replaces this step by an equivariant simplicial Smith-theory âcharacteristic degreeâ, a different formal route. ⢠Six-label triangle systems (§5â6): the forced structure on the complement of any tetrahedron is, by an enumeration reported in the initial extraction, exactly the hemi-icosahedron ââP62RP^2_6 (unnamed in the paper); the 10-label contradiction is a Walkup-style nonexistence of a 10-vertex neighborly 3-pseudomanifold with all facet complements ââP62RP^2_6. Incremental; the Lean proves it by 145 machine-generated case files. Reused. Projector embedding (ConwayâHardinâSloane); partitions of unity; Sard; BorsukâUlam; mod-2 local degree; StiefelâWhitney classes; HinrichsâRichter point adjoining. Caveats. The counterexample is continuous and does not settle finite-set Borsuk in â9R^9. Its convex hull gives a convex-body counterexample, a consequence not discussed in the source. The paper cites an unrefereed AI-assisted GitHub note by Grinsztajn concerning dimension 63, without using it as an input. The literature comparison was limited. 9.3.4 266 ¡ Three mutually unbiased bases in dimension six headline not formalized; NâĄ(6)â¤5N(6)⤠5 formalized | combination | arithmetic and compiler assumptions The source claims NâĄ(6)=3N(6)=3 (Zaunerâs conjecture), as a theorem explicitly labelled âcomputer-assistedâ and conditional on arithmetic and compiler conditions: a C++ pipeline in binary64 with hand-proved one-sided rounding margins, 4,470 seconds on 4 Oct 2026. The headline computation uses neither interval arithmetic nor exact algebra. The companion proves NâĄ(6)â¤5N(6)⤠5 exactly, the MatolcsiâRuzsaâWeiner Fourier-vanishing conjecture for order-6 Hadamard matrices outside Taoâs S6S_6 equivalence class, and Phangaraâs conjecture, with an exact rational verifier; the Lean covers the companion. Extracted instruments. ⢠Seed ball plus fixed-frame completion via a U(2) polar-factor cover (§2â3). Dephase H; cover the nine phases of rows and columns 0â1 by 249,878 balls of radius 0.032 after a minimum-circular-gap normalization; inside a ball write H in 2+4 blocks, the kernels of the 2Ă42Ă 4 blocks are 2-dimensional, the compressed unknown Y=KCââDâKBY=K_C^*DK_B is 2Ă22Ă 2 with trâĄ(6âIâYââY)<0.32tr(6I-Y^*Y)<0.32, hence within p of 6 6 times a unitary VâUâĄ(2)Vâ U(2); an Euler-angle box cover of U(2) with uniform Taylor bounds yields necessary tests. Every order-6 complex Hadamard matrix is represented by 13 parameters with no family assumption, giving a finite cover of the unclassified 25-phase continuum. JamingâMatolcsiâMĂłra proposed discretizing all 25 phases without completing that computation in the work compared by the initial extraction. Combination (polar decomposition, box covers, dual certificates). ⢠Root certificates and tangent/normal refinement (§4â5): a center, a numerical tangent frame and constants such that every exact solution displacement satisfies a normal-component bound, from a residual identity with an approximate left inverse of the Jacobian; âno manifold parametrization is requiredâ. Incremental validated numerics without interval arithmetic. ⢠Injective moments (companion): ÎťâĄ(E)=EâĄ[ReââHâ(ĎâĄ(i),ĎâĄ(j))Eiâj]Îť(E)=E[ReÎ H(Ď(i),Ď(j))^E_ij] over random injections; orthogonality contracts order-one rows; an exact identity 3â|Îł~|2+avgâ|gâĄ(Îą)âgâ(β)|2=03| Îł|^2+avg|g(Îą)g(β)|^2=0 forces either all permuted Fourier values to vanish or HâH H Hadamard, Newtonâs identities force cube roots, and a five-cycle gives Taoâs S6S_6. A Delsarte-type moment certificate in the MatolcsiâWeiner lineage; the Fourier-vanishing claim applies outside the exceptional equivalence class of Taoâs S6S_6 (previously Karlssonâs family only). Combination leaning new. Reused. JMMSW phase discretization and clique search; Rumpâs verified norm bounds; Highamâs rounding analysis; KlappeneckerâRĂśtteler lower bound; Newtonâs identities; Zaunerâs 2-design identity; Weinerâs completion theorem; PeyrlâParrilo rational certificates. Caveats. The headline rests on about 70 pages of hand-derived rounding margins across seven C++ files, not independently rerun or verified for this survey; one condition is checked by inspecting disassembly addresses. The 24 Sept manuscriptâs proof rests on a 4 Oct run; an earlier runâs evidence packet âwas not recoveredâ. The August 2026 classification preprint of CĂĄrdenes WuttigâTindall is cited but is not used in the proof. 9.4 Operator algebras, topology and symplectic geometry 9.4.1 221 ¡ MĂŠzardâParisi formula for diluted spin glasses Lean, 405 files, not in catalogue | new For Poisson-diluted even-arity models whose interaction law satisfies the PanchenkoâTalagrand factorization and positivity hypotheses (model-class conditions, verified for VianaâBray and soft K-SAT, not assumptions on the Gibbs measure), the free energy equals the infimum over finite-depth hierarchical trial laws, with only first-moment integrability. The lower bound is stated for every bounded interaction whose law is permutation invariant, without the even-arity or factorization restrictions needed for the matching upper bound. Under the stated model-class hypotheses, no additional Gibbs-measure factorization assumption is imposed; establishing that factorization is the step Panchenkoâs conditional results left open. Extracted instruments. ⢠Marked-depth Poisson perturbations with prescribed-tree identities (§7, Thm 7.6). Add N3/4N^3/4 bounded single-site factors 1+tνâgâĎi+uνâg0âS01+t_νg _i+u_νg_0S_0 where g, g0g_0 are Âą1Âą 1 functions of Rademacher marks sampled at prescribed depths of an auxiliary L-level hierarchy; the partition function iterates by power means with md=d/Lm_d=d/L. Scores concentrate (EfronâStein, as in GhirlandaâGuerra); a Poisson add-one identity and a two-scale probe t=1/jt=1/j, uâ[jâj,2âjâj]uâ[j^-j,2j^-j] force a limiting analytic function to vanish identically. Shared marks act as sharing indicators, and polarization selects any branching pattern with exact signed coefficients. This extends GhirlandaâGuerra, BarraâDe Sanctis stochastic stability, BarbierâPanchenko side observations and MourratâPanchenkoâs enriched hierarchy (the latter two named in the trace, uncited in the paper). Combination. ⢠Depth shift with charging fresh splits (§8, Lemma 4.5, Thm 8.2). To extract conditional covariances one divides by coefficients of order δ2âbδ^2b; naively the error sum is O(1). Shifting every target branching depth by one level off all old depths forces each target vertex to be created by a fresh unary split of coefficient exactly âδ-δ, so â|cE|â¤Câδ2âbÎŁ|c_E|⤠Cδ^2b and the ratio is bounded. The cost is controlled only on average over regular depth assignments via a vector-martingale energy bound; a three-copy estimate gives induction on leaf count; the limits are strictly ordered NââNââ, then LââLââ, then Ρâ0Ρâ 0. This proves that all finite multioverlaps concentrate given the auxiliary hierarchy, the âfactorizationâ Panchenko 2016 called missing. New, as far as could be determined; the trace marks it as the turning point. ⢠Recursive law encoding of a single site (Lemma 9.1): conditional magnetizations of a uniform site encode an admissible PanchenkoâTalagrand trial law reproducing all prescribed-tree moments. Incremental, a finite-N form of AustinâPanchenko. Reused. Guerra, FranzâLeone and PanchenkoâTalagrand interpolation (upper bound, reproved); AizenmanâSimsâStarr cavity; Panchenkoâs spin-distribution viewpoint; Ruelle probability cascades; EfronâStein. Caveats. The architecture and selected estimates in §8 were inspected, without checking every inequality. The repository supplies a Lean development with review status âuncheckedâ; it was not compiled here. A textual search for admitted proofs would not establish kernel verification. 9.4.2 285 ¡ BaumâConnes and KadisonâKaplansky counterexamples not formalized | combination | reduced assembly-map scope The source constructs a finitely generated torsion-free group GiânâjG_inj, an injection â¤2âGZ^2â G and a degree-2 class pairing to 1 with the torus, such that the Bott class dies in K0â(CrââG)K_0(C^*_rG): rational injectivity of the reduced, coefficient-free assembly map fails. The claim does not contradict classical Novikov or maximal injectivity (HankeâSchick). The source asserts finite generation; it establishes neither finite presentation nor its failure. The corrected AntoniniâBussâEngelâSiebenand result concerns specified exotic group CâC^*-algebras for finitely presented groups; identifying its target with the reduced algebra needs an additional condition, such as exactness, which is also not supplied here. Companions: a torsion-free group with a projection of trace in (0,1/2)(0,1/2) (surjectivity failure, KadisonâKaplansky fails) and a group with p-torsion and an irrational-trace projection. Extracted instruments. ⢠Heisenberg voltage tower with simultaneously sampled Bott symbols (§1â4). The construction begins with a layered bipartite graph labelled by interleaved bit streams with deterministic recovery (Osajda-type word uniqueness with an alphabet small enough that |S|/qâ0 |S|/qâ 0); permutation tables chosen by an L-type sequential law; pruning of âcoherent returnsâ and âbicyclesâ. Each edge gets a voltage in the integral Heisenberg group H and a matrix weight from one distribution whose mean realizes a prescribed torus symbol spread along the central direction, while diffuse horizontal coordinates give every short non-law nontrivial holonomy (SchwartzâZippel on Heisenberg words). Every tower layer carries â2â(H) ^2(H) and incidences become Bott-symbol-valued band operators; the cover is the graphical relator. This extends GromovâOsajda labelled-expander relators (no group-valued coordinates) and GrossâTucker voltage graphs (no analytics). Combination; no prior use of a nilpotent voltage cover of an expander tower as a relator to transport deck-group K-theory was found. ⢠Parity-swindle Bott cancellation in a norm-sequence quotient (§6): four bounded profile families realized by finite Cayley polynomials, two explicit projection paths giving equal K0K_0 classes, finite additivity forcing the height-zero class to vanish; passage through âCrâ/â¨CrâÎ C^*_r/ C^*_r and a âfinite witnessâ lemma. The paper calls it the Eilenberg-swindle pattern of coarse operator K-theory (HigsonâPedersenâRoe). The underlying idea is incremental; its use in this setting is classified as a new combination. ⢠Sheet-cone complex, exact cone chains, prime-order obstruction, Shapiro extension (§5b): cone off sheets, finite peeling gives exactness, a prime-order subgroup would contradict periodicity, so Î is torsion-free; cochain-level Shapiro extends the H2H^2 generator. Incremental. Reused. BaumâConnesâHigson; LĂźckâs trace theorem; an integrality attribution to BartelsâGreenleesâWegner left unresolved by the initial extraction; HankeâSchick; EmersonâHudson; Kasparov descent; graphical small cancellation; Osajda labelling; L; Rieffel projections; DykemaâRørdam. Caveats. The construction uses large parameters (s a multiple of 20,000, scales 2500âHi2^500H_i). Their order of choice and the claimed absence of circular dependence require close checking. All three papers share the architecture, so a defect in it could affect the whole family. The main paper adapts and reproves methods from the KadisonâKaplansky companion, which cites an unrefereed GitHub note as motivation. The comparison used directly retrieved primary sources without a fresh literature search. 9.4.3 293 ¡ Hyperinvariant subspaces and transitive algebras Lean, 1,108-module import closure | new On every infinite-dimensional separable complex Hilbert space there is a nonzero bounded quasinilpotent operator S (âSnââ¤expâĄ(â10ââ(n+1)2/4â)\|S^n\|⤠(-10 (n+1)^2/4 )) with no nontrivial closed hyperinvariant subspace; its commutant is a proper strongly closed transitive algebra, refuting Kadisonâs transitive-algebra problem as well, which the catalogue summary omits. Companion: for every irrational rotation, an operator in the hyperfinite I1I_1 factor with no nontrivial invariant projection in the factor, answering ZhuâFangâShi and the point-mass Brown-measure case left open by HaagerupâSchultz. Nothing is said about the ordinary invariant subspace problem. Extracted instruments. ⢠Backward intertwiner over an ergodic base. S=âŤâSxS= S_x over the 2-adic integers with Haar measure and the odometer xâŚx+1x x+1; each fiber a unicellular bilateral weighted shift with quadratic log-weights plus residue corrections so the cocycle drift has opposite signs at the two ends. V sends eje_j at x to bjâ(x)âejâ1b_j(x)e_j-1 at x+1, where b solves a commuting-square recurrence, normalized per fiber by a supremum finite a.e. by BorelâCantelli but not integrable. Multipliers Lââ(â¤2)âSâ˛L^â(Z_2)â\S\ force any hyperinvariant subspace to be a measurable field of tails KâĽsâĄ(x)K_⼠s(x); VâSâ˛Vâ\S\ gives sâĄ(x+1)â¤sâĄ(x)â1s(x+1)⤠s(x)-1, impossible on a probability space. This extends AtzmonâSodinâs completely indecomposable shifts by transport between fibers. New as a construction; the Bishop-operator literature works in one fiber on invariant, not hyperinvariant, subspaces. ⢠Endpoint-conditioned convolution obstruction (companion, Lemmas 4.1, 4.4): from a putative projection p of trace in (0,1)(0,1), exact convolution identities on orbit pairs, transferred by a Lusin-plus-weak-limit âcompact-set transfer lemmaâ to ordered couplings built from mixed-radix digits; tails bounded without a union bound. This replaces the Brown-measure and DT-operator toolkit. The preliminary assessment is a combination bordering on new; no fresh literature search was completed for it. ⢠Affiliated transport (Lemma 5.1): an unbounded coboundary intertwines two weights on the domain of an affiliated positive operator; invariant projections transport with equal trace via cutoffs. Incremental (Mori 2020). Reused. Domarâs convex-envelope theorems (reproved); DouglasâPearcy equivalence of the hyperinvariant and transitive-commutant problems; Dykema 2005 on projections of hyperinvariant subspaces; AnantharamanâPopa crossed products; BorelâCantelli; FejĂŠr kernels. Caveats. The repository provides two formalization routes; neither was compiled or kernel-checked for this survey. The companionâs estimates (m(7/10)âm^(7/10)m, m1000m^1000) were not independently verified. Remark 1.5 asserts a published 2017 corollary is false. The companion estimates and comparisons with earlier equivalence claims require further checking. 9.4.4 297 ¡ Naimarkâs problem in ZFC Lean, 16 modules, not in catalogue | combination | earlier related result: Tanaka The source constructs a unital, infinite-dimensional, simple CâC^*-algebra with a faithful tracial state whose nonzero irreducible representations are all unitarily equivalent, in ZFC alone. AkemannâWeaver 2004 needed Jensenâs diamond. The construction has length + c^+; density is left in [,+][ c, c^+]. Tanakaâs preprint of 22 September 2026 [5] gives the same existence theorem plus density exactly c; the paper acknowledges this earlier result. Extracted instruments. ⢠Selective bridge via reduced HNN adjunction along peaking sequences (Thm 4.1). A decreasing projection sequence âpeaks toâ a state h if h is the only state with value 1 on all of them. Let A be a unital CâC^*-algebra with a faithful tracial state and no finite-dimensional irreducible representations. For two inequivalent pure states, take decreasing peaking projection sequences starting at 11, with equal traces 1=t0>t1>âŻ>01=t_0>t_1>¡s>0 tending to zero. The source adjoins an intertwiner carrying one sequence onto the other via Uedaâs reduced HNN extension (a corner of an amalgamated free product). The claim is that every old pure state extends uniquely, lifts are pure, and the only new equivalence is between the two chosen classes; simplicity and a faithful trace-preserving expectation are preserved. The proof uses norm decay on reduced words via excision, cross-excision, trace-null supports and âmoving the peak through the stable letterâ. This replaces AkemannâWeaverâs crossed product by a KishimotoâOzawaâSakai automorphism of the whole algebra, which forced separability at each stage and hence âľ1 _1 and diamond. CalderĂłnâFarahâs Question 8.1 asked for exactly such a partial crossed product. The initial extraction classifies this as a combination; a detailed comparison with Tanakaâs construction remains necessary. ⢠Dependency-closed subiterations with reduced-HNN reordering (Prop 3.4, Thm 5.5): each step records a countable set of earlier steps it depends on; adjunctions with data in a common base commute, so omitted steps can be postponed; every pure state of the big algebra is the unique extension of a pure state on a separable dependency-closed subalgebra. This supplies the ingredient CalderĂłnâFarah §8 identified. The initial extraction classifies this organization as a new combination, with a CâC^*-analogue of elementary-submodel closing-off. ⢠Diamond replacement: length + c^+, a fixed injective schedule, ⤠c pure states per stage; no guessing principle at all. Incremental. The same argument appears to run at length c, which would give density c as in Tanaka; this possible strengthening is not proved here or stated in the paper. Reused. Uedaâs HNN extensions and BlanchardâDykema expectations; AkemannâAndersonâPedersen excision; AkemannâWeaver cross-excision; Kadison transitivity; KishimotoâOzawaâSakai homogeneity (only on separable subalgebras; reproved in Lean). Caveats. The repositoryâs formalization records differ: the catalogue omits the result, while the documentation reports full coverage. No Lean build was run here. 9.4.5 309 ¡ Kervaire invariant at the prime three not formalized | combination | claims a new element exists With bjâExt2,4â 3j+1b_j ^2,4¡ 3^j+1, the survivors are exactly jâ0,2,3jâ\0,2,3\: b1b_1 dies (Toda), bjb_j dies for all jâĽ4j⼠4, and b3b_3 survives, giving an order-three element in Ď322âS(3) _322S_(3). This is a finite survivor list with a missing index j=1j=1; the odd-primary Adams-family indexing differs from the classical prime-two Kervaire invariant convention. The result would also refute BelmontâRayâs Conjecture 0.1(3). HHRâs 2011 odd-primary note explicitly left θ4 _4 at p=3p=3 open. Extracted instruments. ⢠Finite Euler bound: take the coefficient of x27x^27 in the strict coordinate change between two orientations of the norm NeKâMâUN_e^KMU, norm and counit it to a class whose geometric fixed points vanish, so isotropy separation gives aÎťdâz=0a_Îť^dz=0; it maps to a unit in Borel E6E_6, so aÎť235=0a_Îť^235=0 and the Euler-localized homotopy fixed point spectral sequence must kill 1 by an explicit differential. This replaces HHRâs Gap and Periodicity theorems and avoids any Tate-convergence claim. Combination: norms, geometric fixed points and isotropy separation are HHR and MeierâShiâZeng; using a coordinate-change coefficient as nilpotence witness had no matching precedent in the initial comparison. ⢠Exact cyclic coefficient model and fixed geometry: proves Eââ (W(k)[x0..x8,Îâ1]/(xi+xi+3+xi+6))â§E_* (W(k)[x_0..x_8, ^-1]/(x_i+x_i+3+x_i+6)) with the C9C_9 action xiâŚxi+1x_i x_i+1 (the BelmontâRay coefficient conjecture), then shows the Ď-eigenspace is a strict formal module deformation of relative height 3 whose DieudonnĂŠ crystal determinant carries a sign character, excluding equivariant maps that could be differentials. This proves a stated conjecture by a combination of methods (Hill 2007 sketched formal-module deformations conditionally). ⢠Lattice forcing from the known survivor: after d33d_33 the Tate pages are a finite array of fifteen labels modulo permanent unit translations; a mod-4 normalizer character and a parity count fix Îş=â1Îş=-1; the detector of b2b_2 must be hit by d93d_93, forcing an outgoing differential on the whole lattice containing every jâĽ4j⼠4 detector. The paperâs key insight: a sphere class âcan acquire an incoming differential after passage to Tate localizationâ, so one must show outgoing, not vanishing. Combination or unclear; rests on exhaustive hand tables through d313d_313. Reused. AdamsâNovikov spectral sequence; MillerâRavenelâWilson 2-line; Toda differentials; BelmontâRay CM detection via LubinâTate; Selickâs criterion; Amelotteâs θ3 _3; the positive branch uses a truncated extended-cube construction from the stem-106 element, followed by Moore-spectrum and AdamsâNovikov corrections (23,384 unknowns in the finite calculation). This produces stem 3â 108â2=3223¡ 108-2=322; the ordinary ring cube would lie in stem 3â 106=3183¡ 106=318 and is not the claimed new element. Caveats. The claimed conclusion includes a new stable homotopy class. Its verification requires about 1,700 lines of differential calculations, with several statements specified only âup to nonzero scalarâ entering a sign-sensitive character test. Although the paper has a reproducibility section, no code is supplied. 9.4.6 325 ¡ The complete Crouzeix conjecture Lean, all sizes, matrix-valued, arbitrary Hilbert space | combination leaning new For every bounded operator A on a nonzero complex Hilbert space, including infinite-dimensional spaces, and every matrix polynomial PâĄ(z)=âkBkâzkP(z)= _kB_kz^k, the stated complete inequality is ââkAkâBkââ¤2âsupzâWâĄ(A)âPâĄ(z)â=2âmaxzâWâĄ(A)ÂŻââPâĄ(z)â. \| _kA^k B_k \|⤠2 _zâ W(A)\|P(z)\|=2 _zâ W(A)\|P(z)\|. The constant 2 is sharp. The numerical range need not be closed in infinite dimension, which is why the supremum or its closure is used. The holomorphic extension concerns matrix-valued functions holomorphic on an open neighborhood of WâĄ(A)ÂŻ W(A); rational functions must have all their poles outside WâĄ(A)ÂŻ W(A). In this sense the closure is a complete 2-spectral set. Scalar proofs are presented in the 2026 preprints of Jin, LoristâSchwenninger and Luo [7, 8, 9]. LoristâSchwenninger explicitly explain why their proof and Jinâs do not directly give the completely bounded version. Extracted instruments. ⢠Ordered density comparison (direct paper Thm 3.2, main Lemma 5.1). For a finite matrix A and a matrix polynomial F normalized to have boundary supremum norm one on an enclosing analytic convex domain, choose a unit top singular pair FâĄ[A]âx=ÎłâyF[A]x=Îł y (the zero case is immediate). Compress the CrouzeixâPalencia positive field R+Râ⪰0R+R^* 0 by [XâY][X\ Y] into a 2Ă22Ă 2 block Î (Îť) of mĂmĂ m boundary functions whose entries have Faber coefficients Pk=Xââbkâ(A)âXP_k=X^*b_k(A)X, Mk=Yââbkâ(A)âXM_k=Y^*b_k(A)X. For PSD Î , trâĄ(ÎâJâÎâJ)âĽ0tr( J J)⼠0 gives 2â|M+Lâ|HâS2â¤|P+Pâ|HâS2+|âQ+Qâ|HâS22|M+L^*|^2_HSâ¤|P+P^*|^2_HS+|Q+Q^*|^2_HS; integrate over the circle and apply Parseval. The cross term is at least a2=â|Mk|2a^2=ÎŁ|M_k|^2; the diagonals are bounded by testing the functional on the two ordered products FG and GF (so no commutation is needed), with the Faber weight 2 giving â¤4âa2/Îł2⤠4a^2/Îł^2. Hence 2âa2â¤8âa2/Îł22a^2⤠8a^2/Îł^2 and Îłâ¤2γ⤠2 when a>0a>0. If a=0a=0, the cross functional vanishes, so its value on F gives Îł=0Îł=0. The bounded-operator conclusion is obtained through finite compressions and approximation, without assuming a norm-attaining vector in infinite dimension. This replaces CrouzeixâPalenciaâs operator-norm triangle inequality (1+21+ 2) and LoristâSchwenningerâs perturbation lemma, whose commutation hypothesis âis not available after matrix amplificationâ. Combination leaning new: extremal pairs and the positive double layer are known; measuring the compressed block in boundary L2L^2(HilbertâSchmidt) had no precedent in the literature examined. ⢠Exterior Faber coefficients and the positive kernel: the KĂśvariâPommerenke and Beckermann weight-2 bound transplanted from HâH^â to matrix L2L^2. Incremental. ⢠Optimal metric and endpoint extremal (main Thm 1.2): for a finite matrix and a bounded convex domain with regular real-analytic boundary strictly enclosing its numerical range, the Stein LMI attains the squared minimal condition number, with Îşâ[1,2]Îşâ[1,2]; SDP duality plus a unitary-colligation realization gives an exact extremal; a common positive boundary representation follows from Sz.-Nagy. Combination of textbook interpolation theory. Reused. DelyonâDelyon and CrouzeixâPalencia double-layer positivity; exterior conformal maps and Faber polynomials; Paulsenâs similarity theorem; Stein 1952; Sz.-Nagy dilation; KatsnelsonâKheifetsâYuditskii colligations. Caveats. The structural theorem applies separately to each enclosing domain strictly containing WâĄ(A)ÂŻ W(A); no limiting similarity on the closure is asserted. Luoâs scalar argument also uses a top singular pair [9], so that ingredient alone is not evidence of novelty. The relation between its boundary certificates and the matrix-valued argument here requires closer comparison. 9.4.7 340 ¡ Counterexample to the nearby Lagrangian conjecture not formalized | combination For some large even N, Q=S9ĂSNâ1Q=S^9Ă S^N-1 admits a closed exact embedded Lagrangian LâTââQLâ T^*Q, diffeomorphic to Q, not Hamiltonian isotopic to the zero section. The paper does not address smooth isotopy or whether the projection is homotopic to a diffeomorphism. N is not explicit and L depends on a non-constructively chosen homotopy class. The comparison with Ălvarez-GavelaâIgusaâSullivanâs construction concerns the passage from Legendrian to embedded Lagrangian families [11]. Extracted instruments. ⢠Momentum-separation embedding of a tube family (Prop 4.2). From a family gbg_b, bâS9bâ S^9, of degree-2 homogeneous functions on âNR^N whose negative domains form a nonstandard smooth tube family, define the Morse family FâĄ(b,v,w)=Gbâ(w)âRâĄ(b)âβâ(|w|/T)ââ¨v,wâŠF(b,v,w)=G_b(w)-R(b)β(|w|/T) v,w with RâĄ(b)=ÎâeKâθâ(b)R(b)= e^Kθ(b), θ a height function. Homogeneity makes the critical locus a copy of S9ĂSNâ1S^9Ă S^N-1; equal sphere momenta force wâwâ˛|vw-w v, and the base momenta separate the pair unless b is near a pole, where gbg_b is quadratic and the critical equation has a unique solution. This converts a nontrivial tube family into an embedded exact Lagrangian, the step AIS could only do for Legendrians via wrinkling. Combination; the exponential scale over the parameter sphere is the paperâs own device. ⢠One-critical-point rigidity (Prop 3.1): a family over S9S^9 of functions homogeneous at infinity with exactly one nondegenerate critical point per fiber and trivial stable spherical class has trivial stable tube class, via Adamsâs injectivity of J8J_8, a family of h-cobordisms thickened into a fixed cylinder, Igusa stability (through CourteâPorcelliâs bounds) and parametric multijet transversality. Incremental over Kraghâs identification of one-critical-point functions with the homotopy fiber of the HatcherâWaldhausen map. ⢠Torsion-invisible kernel class (Prop 2.2): Ď10âWâhdâiâfâfâ(â)(2) _10Wh^diff(*)_(2) has order 32 (Rognes) while the cokernel of J9J_9 has order â¤4⤠4, so a nonzero class exists in the kernel of the tube fibrationâs map to BG; degree 9 is chosen so J8J_8 and J9J_9 are injective. A 2-torsion class invisible to AISâs real-valued tube torsion. Combination of standard computations. Reused. Waldhausenâs tube theorem; WaldhausenâJahrenâRognes stable parametrized h-cobordism theorem; Rognes 2002; Adams; Igusa; SikoravâChaperon generating-function transport; Bott periodicity. Caveats. The argument depends on 2025â26 preprints by AIS, AbouzaidâĂlvarez-GavelaâCourteâKragh and CourteâPorcelli, including an informal comparison between models. Corner and stabilization conventions require detailed checking; the detection argument depends on them. 9.4.8 376 ¡ Universal computation in forced NavierâStokes flows lemmas formalized; main paper not | incremental For each fixed positive computable viscosity ν, an effective procedure maps a Turing machine and input to a smooth mean-zero force on 3T^3, time-independent for tâĽ1t⼠1, such that NavierâStokes from rest has a global smooth solution and a marked material particle enters a fixed region in finite time iff the machine halts. Variants: â3R^3 with compact support, force decaying faster than any power, an Eulerian velocity observer. The family contains nine closely related manuscripts. Extracted instruments. ⢠Injective local compiler: a three-track history-recording alphabet with a return-mark bit so that destination state and written symbol determine the incoming rule, making Moore-type target rectangles pairwise disjoint on the whole tape domain. This is an explicit implementation of Bennett 1973 history recording and is classified as incremental. ⢠Effective parking and routing isotopy: compactly supported Hamiltonian pulses (translation and reciprocal-diagonal generators) and 3D localized curls that extract sources to parking columns, rescale, and insert at targets without collision, giving a smooth volume-preserving time-periodic field whose period map is the prescribed affine map near each rectangle. This combines standard box-moving by Hamiltonian isotopies with an effective description of the construction. ⢠Scale-nested memories under rapidly vanishing forcing: unit-length physical steps but the n-th configuration written at digit scale 2âsn2^-s_n with displacement much smaller, so derivatives vanish faster than any power while computation continues; old records retained at coarser scales; coordinates alternate roles. The initial extraction identifies this elementary construction as the familyâs clearest candidate new instrument. Reused. Mooreâs generalized shifts and gapped radix coding; Turingâs printing problem; Lerayâs energy uniqueness; HelmholtzâLeray projection; heat-kernel bounds. Caveats. For a chosen smooth divergence-free U with UâĄ(0)=0U(0)=0, setting f=Ut+(Uâ â)UâνÎUf=U_t+(U¡â)U-ν U makes the NavierâStokes identity hold with zero pressure. This residual construction does not automatically establish the required mean-zero condition, effective description, bounded derivatives, spatial support, eventual stationarity or time decay of the force; the properties prescribed in each version still require proof. Stationary Euler solutions are not generally Beltrami. The cited CardonaâMirandaâPeralta-SalasâPresas construction uses Beltrami fields, a special class of stationary Euler flows, to realize computation. The forced constructions therefore have a different scope from that construction and from unforced or low-mode-controlled flows. Computation is exact-real reachability with no finite-precision tolerance, as the papers concede. No fresh literature search was completed for this entry. 10 Verification and dependency scoreboard The table preserves the initial extractionâs classification, with source-status corrections where checked. âYesâ and file counts report repository artifacts or textual assessments from the initial extraction; they do not imply compilation or a complete dependency-closure check during either stage. The original labels mark 19 of the 38 rows as headline-formalized: 003, 017, 087, 102, 107, 157, 158, 196, 197, 248, 287, 362, 103, 112, 156, 221, 293, 297 and 325. Coverage inspected for 003 and 087 was partial (the zeta declaration and symmetric Mahler result respectively), so 19 cannot be read as 19 fully inspected family claims. The original companion-only classification has five families: 143, 159, 263, 266 and 376. The rule counts a family once when its original row records a companion result or supporting lemmas but no headline coverage; including the lower-bound companion in 159 gives five, while excluding it gives four. These are counts of the original labels, not a current formalization census. In particular, the inspected snapshot also links a reciprocal-sum headline development for 159 and reports coverage for 007. The subsequent mathematical review did not include building or fully checking those developments, so their presence is recorded separately rather than silently changing what was checked. Table 4: Verification and dependency scoreboard (initial extraction labels with selected source corrections). Family Lean label Statement faithful? Depends on other OpenAI papers? Uncited nearest ancestor 003 zeta partly inspected; Dirichlet/Hecke declarations also located not inspected no (cubic first-moment paper cited, unused) â 004 no â yes: FM modularity at 2; pointwise 2-converse â 017 867 files, not in catalogue yes (eventual bound and sSup form) no Masser 1981; FischlerâNakamaye 2014 032 no â no load-bearing (family 001 in a remark only); withdrawn papers never cited â 074 no â 3D: alternative route only. 4D: cites 3D for a lemma that is really GWZ 2026 RiosâSawyer 087 original: symmetric; general/polar modules supplied, unbuilt symmetric statement only in initial extraction no â 102 475 files; PCP and KMS reproved yes, full UGC no â 107 supplied; unbuilt here yes, straight-line programs over âC no AlmanâLi 2026 157 276 files yes, Mathlib chromatic number and clique minors no â 158 â24,500â 24,500 lines yes, unrestricted no â 159 original: lower-bound companion; headline also linked, unbuilt â no load-bearing â 196 124 files incl. the classifying complex yes no â 197 125 files; search terminates at hâ¤217h⤠217 yes (non-soficity excluded) type-F corollary only â 248 yes, F from scratch yes corollaries only â 287 77 modules, in docs not catalogue reads faithful no (family 298 later, uncited) â 304 no â no â 362 207 files, continuation statement included yes; uniqueness among global classical solutions no CheverryâIbrahim 2025 Second group 002 no â yes: Selmer converse, two-primary BSD, Goldfeld (â Smith 2025 preprint) â 007 original: statements; docs report coverage, unbuilt â no â 010 no â main paper none; pro-modularity satellite depends on main + Hecke-dimension. External: Thorne Aug 2026 (unrefereed) â 040 no â no (two unrefereed competing preprints cited, not used) â 103 39 files; identifiers obfuscated yes, multi-tape TM, L=RLâ§RL=BPLL=RL =BPL no â 112 179 files yes, ÎŁ3 _3 gate count, exact computation no â 143 companion (quintic LiĂŠnard) only â no â 156 275 files, exact reals yes, compact set, diam 2 2, no ten-cover no (unrefereed GitHub note cited, not used) Ky Fan-type refinements 193 no â no (Lech paper cited as related) SuslinâVoevodsky orbit lemma 221 405 files, not in catalogue yes, faithful statement no MourratâPanchenko; BarbierâPanchenko 263 companions only (607 + 428 files); headline none companions faithful companions depend on main paperâs foundation estimates â 265 no â PEPS companion depends on main â 266 companion (NâĄ(6)â¤5N(6)⤠5, Fourier vanishing outside Taoâs S6S_6 class) only â no â 268 no (computer-assisted, Python verifier) â companion depends on mainâs intermediate data â 285 no â methodological on the KadisonâKaplansky companion; none on 196/197 â 293 1,108-module closure, two formal routes yes mutual elementary lemmas with companion â 297 16 modules, not in catalogue yes, no hypotheses no Tanaka, arXiv 2609.26930 309 no â no â 325 199 files, five challenges yes, full cb statement no Luo 2026 (novelty comparison incomplete) 340 no â no; external: AIS, AACK, CourteâPorcelli 2025â26 preprints â 376 4 of 9 manuscripts, engineering lemmas â dependencies among nine public manuscripts; main self-contained AgrachevâSarychev (not engaged) Comparator challenge files contain target statements, often with sorry placeholders. Their JSON configurations point to separate solution modules; a placeholder in a challenge does not determine whether its solution is complete. For example, GeneralMahler.json points to a solution theorem distinct from its challenge, and the 003 configurations point to zeta, Dirichlet and Hecke declarations. These files were read, not compiled, and their transitive dependencies were not exhaustively inspected. Textual inspection and standard-axiom configurations do not establish kernel verification of the 19 labeled families. The configurations inspected in the subsequent mathematical review disable the optional nanoda recheck. 11 Limits of the extraction and mathematical review ⢠Reading is not verification. The initial extraction and subsequent mathematical review included checks of selected statements, hypotheses and identities; those checks do not independently certify every underlying proof. No Lean formalization was built or kernel-checked during either stage. Absence of a check in this survey says nothing about whether other people have checked a manuscript. ⢠Novelty assessments depend on the search scope. âNo precedent foundâ means that the literature comparison described in the card found no matching instrument; a device in a 1980s Russian paper or an unpublished talk could be missed. The verdicts are provisional judgments relative to the literature searched; the subsequent mathematical review did not independently validate them, and mixed labels are not counted as disjoint classes. ⢠Choice of thirty-eight. The release has 372 families; this set was selected for the prominence of the problems, which favors major conjectures and particularly strong claims. Families centered on improvements to existing bounds were not examined systematically. ⢠Search coverage. Some entries in the second group used directly retrieved primary sources without a fresh literature search. Their novelty assessments have correspondingly narrower support. ⢠Priority and AI lineage. At least four results have close human or AI-assisted neighbours predating the release (Naimark: Tanaka; Crouzeix: Jin, LoristâSchwenninger, Luo; Borsuk: a 63-dimensional GitHub note; Serre positivity: a December 2025 AI note). This survey records these; it does not adjudicate priority. ⢠Scope of the extracted novelty. The extraction identified devices within proofs. It did not identify a new foundational theory, a new category of object comparable to motives or perfectoid spaces, or a new conjecture. This describes what the extraction found in the selected families; it is not an exhaustive claim about their contents or the full release. 12 Conclusion and future directions This paper extracts candidate new mathematical instruments from 38 families in OpenAIâs October 2026 release. The family entries describe their roles, antecedents and caveats; the maps, eleven cross-cutting patterns and dependency scoreboard make those descriptions easier to compare. The initial assessments identify new constructions and proof mechanisms, applications of established theorems in different settings, and adaptations whose earlier sources need closer acknowledgment. These findings remain subject to the limits of the literature comparisons and mathematical checks reported here. The project begins with extraction and then asks what can be established and used. The signed-restriction case study illustrates that sequence: an instrument identified in a source paper becomes an input to a further theorem. This is the reason to investigate the release as a treasure mine. Three directions would extend the work: (1) Independent verification. The cards identify where human checking would matter most: headline proofs not independently checked here (among them Hilbertâs tenth problem over âQ, the rational Hodge conjecture for CM abelian varieties, Kakeya, ErdĹsâs reciprocal-sum conjecture, HilbertâSmith and the general Mahler conjecture), load-bearing dependencies on other unverified manuscripts (for example family 004 on family 010), and specific flagged steps such as Proposition 5.14 of family 002 or the proposed extension of family 017 to ÎźâĄ(logâĄr)=2Îź( r)=2 for rââ>0â1r _>0 \1\, which requires a separate argument. Expert refereeing of these points, and of the novelty verdicts based on incomplete literature searches, would strengthen these assessments. (2) Formalization. The nineteen original headline labels include partial inspection for 003 and 087 and are not a count of fully verified results. Repository documentation and linked solution modules should first be reconciled theorem by theorem, including the additional coverage reported for 007 and 159, then compiled and kernel-checked independently. Companion proofs must be kept separate from their familiesâ headline statements. (3) Extending the extraction to all 372 families. The extraction covers a sample selected for prominent problems. Applying the same protocol to the whole release, including families that improve existing bounds, would turn the catalogue of instruments into a comprehensive, searchable resource, indexed by mechanism as well as by problem, and would test whether the patterns found here hold across the release. Acknowledgments Claude Fable 5.1 was used for the initial extraction of mathematical instruments, literature comparisons and preliminary novelty assessments. The author thanks OpenAIâs GPT-6 for assistance with mathematical review and draft revision. The author takes responsibility for the establishment of this research direction, design of the methodology, the curation and interpretation of the extracted material, the development of the use case studies, and the presentation of the final manuscript. References [1] Repository: github.com/openai/math, catalogue overview.pdf, manuscript map CONTENTS.md, Lean catalogue lean/formalization.yaml, history.md (withdrawals of 7 Oct 2026). Source comparisons for this revision use commit fd4aeeb2e4fc729c18d98444fed42fd0529eeeb. The initial release contained 722 manuscripts; the inspected snapshot lists 719 after three withdrawals, still in 372 families. [2] Paper directories under preprints/, by family: 003 The-Quasi-Riemann-Hypothesis-October-5-2026; companion: The-Quasi-Riemann-Hypothesis-September-30-2026 004 Hilberts-tenth-problem-over-the-rational-numbers-October-6-2026 017 The-irrationality-exponent-of-pi-is-2-September-24-2026 032 The-rational-Hodge-conjecture-for-CM-abelian-varieties-October-6-2026 074 The-Kakeya-maximal-conjecture-in-three-dimensions-September-23-2026 and Every-four-dimensional-Kakeya-set-has-full-Hausdorff-dimension-September-24-2026 087 The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026; The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026; Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026 102 The-Unique-Games-Theorem-September-23-2026 107 Matrix-Multiplication-Nine-Fourths-October-2-2026 157 A-counterexample-to-Hadwigers-conjecture-September-23-2026 158 The-Euclidean-plane-is-not-five-colorable-September-23-2026 159 Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026 196 A-Torsion-Free-Group-Algebra-with-Zero-Divisors-September-23-2026 197 A-Counterexample-to-Kaplanskys-Direct-Finiteness-Conjecture-in-Characteristic-Two-September-23-2026 248 Thompsons-group-F-is-nonamenable-September-23-2026 287 An-isomorphism-of-the-free-group-factors-September-23-2026 304 The-Hilbert-Smith-conjecture-in-every-finite-dimension-September-23-2026 362 Global-classical-solutions-of-the-three-dimensional-relativistic-Vlasov-Maxwell-system-September-23-2026 [3] Second group, under preprints/: 002 Exact-Birch-Swinnerton-Dyer-Formula-from-Low-Selmer-Corank-October-7-2026 007 Ordinary-two-point-correlations-of-multiplicative-functions-September-24-2026 010 Fontaine-Mazur-modularity-at-the-prime-2-October-6-2026 040 Blochs-Conjecture-for-Surfaces-with-pg-equals-q-equals-0-September-24-2026 103 Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026 112 Beyond-the-Square-Root-Exponent-for-Depth-Three-Boolean-Circuits-September-23-2026 143 uniform-bounds-for-planar-polynomial-limit-cycles-September-24-2026 156 A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026 193 Positivity-of-Serres-Intersection-Multiplicity-September-23-2026 221 The-Mezard-Parisi-formula-for-diluted-spin-glasses-September-23-2026 263 Uniform-excess-charge-for-Coulomb-molecules-and-the-outer-radius-of-neutral-atoms-September-24-2026 265 A-two-dimensional-area-law-from-a-global-spectral-gap-September-24-2026 266 The-maximum-number-of-mutually-unbiased-bases-in-dimension-six-September-24-2026 268 The-periodic-spin-one-Haldane-gap-September-24-2026 285 A-Torsion-Free-Counterexample-to-Reduced-Baum-Connes-Injectivity-September-23-2026 293 Backward-intertwiners-and-a-transitive-commutant-September-27-2026 297 A-counterexample-to-Naimarks-problem-in-ZFC-September-24-2026 309 The-Kervaire-Invariant-Problem-at-the-Prime-Three-September-24-2026 325 The-complete-Crouzeix-theorem-September-23-2026 340 A-counterexample-to-the-nearby-Lagrangian-conjecture-September-23-2026 376 Universal-Computation-with-Eventually-Stationary-Navier-Stokes-Forcing-September-27-2026 [4] OpenAI. Released abridged reasoning summaries in the public math repository, directory reasoning_traces/ (snapshot identified in reference [1]). This survey uses nine summaries: families 007, 017, 087, 102, 159, 197, 221, 287 and 362. The inspected repository lists ten summaries in total, additionally including family 271; nine is the selected count, not the repository total. [5] R. Tanaka. A separably representable counterexample to Naimarkâs problem in ZFC. 2026. arXiv:2609.26930v1. [6] J. A. Thorne. Towards the FontaineâMazur conjecture for GL(2). 2026. arXiv:2608.07186v1. [7] S. Jin. The numerical range is a 2-spectral set. 2026. Preprints.org 202607.1919, version 4. [8] E. Lorist and F. L. Schwenninger. A solution to Crouzeixâs conjecture. 2026. arXiv:2608.03841v2. [9] Q. Luo. Two boundary-certificate proofs of the Crouzeix theorem: Fiberwise Fourier recurrence and defect-Gram telescoping. 2026. Preprints.org 202608.1661, version 2. [10] F. Illingworth and R. Steiner. Disproof of the dominating Hadwiger conjecture. 2026. arXiv:2609.35361. [11] D. Ălvarez-Gavela, K. Igusa and M. G. Sullivan. Legendrian and Lagrangian higher torsion. 2026. arXiv:2603.28007v2.