Release examined: October 6, 2026. Evidence status: Source reporting and selected static proof-artifact inspection; no independent Lean execution by Kingy.
OpenAI has published a mathematics repository containing 722 manuscripts grouped into 372 result families. Its catalogue claims resolutions of problems across number theory, geometry, theoretical computer science, algebra, mathematical physics and differential equations. Among them are the Mahler conjectures, an exact irrationality exponent for π, the Unique Games Conjecture, the free group factor isomorphism problem and large-data global regularity for the relativistic Vlasov–Maxwell system.
The release also contains Lean proof artifacts and ten abridged reasoning summaries. That makes it possible to examine considerably more than a list of impressive theorem names. It does not make every manuscript an independently accepted result.
The most useful reading of this release is a large collection of mathematical claims with differing levels of supporting evidence. Some claims have selected formal statements and proposed proof implementations; others currently rely on manuscripts. OpenAI itself warns that unformalized results may contain issues. The formalization manifest records partial progress and an unchecked review status.
For readers asking what this cost, the public answer is unusually specific in one respect and incomplete in several others. OpenAI reports an average of three hours of ChatGPT Pro thinking compute per result with an unreleased internal model, across an evaluation in which it posed approximately 4,000 problems. It does not disclose an aggregate dollar cost, token count, accelerator-hour total or training budget. OpenAI’s release notes
This article examines the October 6, 2026 release snapshot. It explains the major claims, the reasoning and proof techniques behind selected results, the limits of the formalization evidence, and the resource accounting that can and cannot be reconstructed. A complete index of all 372 families appears at the end.
What OpenAI released, and what the counts mean
A manuscript is a document. A result family groups related documents. One family can contain a principal theorem, a different proof, an application, a strengthened version and a companion argument. Those are useful distinctions when a release contains hundreds of papers.
Kingy’s catalogue count reproduces the 372 family entries. The repository’s preprint directory contains 722 manuscript directories. The overview distributes the families across 17 mathematical disciplines. Family numbers retain gaps: the highest ID is 377, while IDs 045, 061, 070, 123 and 163 are absent from this snapshot. Using the largest ID as the family count would therefore be wrong. Release catalogue
The manuscripts also have their own dates. Several selected papers are dated in September, while others are dated October 3–5. October 6 is the catalogue’s release date; it should not be treated as the date every argument was created.
The approximately 4,000 problems are a third unit. They describe the evaluation’s inputs. OpenAI says it aggregated the outputs and applied a significance requirement to produce the released catalogue. It does not publish a complete problem-by-problem outcome table. Consequently, 372 divided by 4,000 is a family-to-input ratio, not a verified solve rate. Dividing 722 by 4,000 would instead count manuscripts against problems, with the same underlying mismatch.
The discipline breakdown is reproduced below. These are family counts, calculated from the overview, rather than paper counts or counts of independently verified breakthroughs.
| Discipline | Result families |
|---|---|
| Number theory | 31 |
| Algebraic and complex geometry | 36 |
| Real and complex analysis | 16 |
| Convex and metric geometry | 15 |
| Theoretical computer science | 40 |
| Dynamical systems and ergodic theory | 12 |
| Combinatorics | 37 |
| Algebra | 18 |
| Probability and statistical mechanics | 29 |
| Mathematical logic | 6 |
| Group theory | 14 |
| Mathematical physics | 25 |
| Operator algebras | 19 |
| Topology | 18 |
| Functional analysis | 11 |
| Differential geometry | 29 |
| Partial differential equations | 16 |
| Total | 372 |
The largest category is theoretical computer science, with 40 families. Combinatorics has 37, algebraic and complex geometry 36, and number theory 31. The breadth matters: assessing this collection requires expertise across subjects whose proof standards, background libraries and familiar failure modes differ.
The major mathematical claims, with their scope intact
The following sections use “claims” deliberately. They report what the released manuscripts and scope notes assert. Kingy has inspected source material and selected proof entry points; we have not independently proved these theorems, rerun the full Lean library or obtained referee acceptance for the collection.
A fixed zero-free region for zeta, rather than the full Riemann Hypothesis
Family 003 claims that every Dirichlet L-function, including the Riemann zeta function, has no zeros in the half-plane Re(s) > 7/8. The same region is asserted for finite-order Hecke L-functions over the field ℚ(√−3), allowing the principal pole at s = 1. A companion manuscript gives an alternate argument for Re(s) > 11/12. Zero-free-region paper
The full Riemann Hypothesis says that all nontrivial zeta zeros have real part 1/2. A fixed boundary at 7/8 would be a substantial zero-free result, but leaves a wide region between 1/2 and 7/8. It cannot establish the full hypothesis. Clay’s problem description
The paper’s central device compares the same character-sum signal in two ways. One calculation bounds the sum directly; another connects it to a Mellin integral involving the reciprocal of an L-function. The claimed power savings allow the reciprocal to continue across a hypothetical rightmost zero, producing a contradiction. The later argument uses a compensated probe and marked estimates to reach seven eighths.
The scope page separately describes a uniform logarithmic exclusion region for Landau–Siegel zeros. That means excluding real zeros sufficiently close to one, with a positive constant independent of the conductor. It does not mean excluding every real zero throughout (0,1), and the selected statement gives no explicit numerical constant. Family 003 formalization scope
Hodge results for CM abelian varieties and products of K3 surfaces
Family 032 claims the rational Hodge conjecture for every complex abelian variety with complex multiplication, in every dimension and codimension. The family also contains claims for arbitrary products of projective complex K3 surfaces and the algebraicity of their Kuga–Satake correspondences. These are specific classes of algebraic varieties, with broad consequences if the arguments hold. CM Hodge paper
The full rational Hodge conjecture concerns smooth projective complex varieties generally. Its claim is that rational cohomology classes of the appropriate type arise from rational combinations of algebraic cycles. Covering CM abelian varieties does not cover every variety in that statement. Clay’s Hodge description
In the selected CM paper, the proof roadmap reduces balanced cohomological tensors to elementary four-factor relations. It proposes algebraic representatives using surface constructions and nonzero period pairings, then composes correspondences, contracts auxiliary factors and descends coefficients to recover the original classes. The paper invokes established implications through Milne’s work to claim the Tate conjecture for abelian varieties over finite fields and the Hodge standard conjecture for abelian varieties in arbitrary characteristic.
OpenAI identifies work on Hodge for CM abelian varieties as an exception to its otherwise common result-generation procedure. There is no per-paper compute account for that exception in the release notes. Also, this snapshot has no lean/docs/032.md family scope page. That is an observation about the published mapping, rather than proof that no relevant formal material exists anywhere in the library.
Birch–Swinnerton-Dyer under low-Selmer-corank hypotheses
Family 002 claims the full Birch–Swinnerton-Dyer leading-term formula for elliptic curves over ℚ whose full q-power Selmer group has corank zero or one for some prime q. It includes equality of the relevant ranks and finiteness of the Tate–Shafarevich group. “Full” here describes the leading-term formula within the stated range, including all its prime factors. Low-corank BSD paper
The Selmer condition is essential. This does not assert the formula for every elliptic curve of arbitrary rank. The broader BSD problem connects rational points on an elliptic curve to the behavior of its L-function. Clay’s BSD description
Family 006 separately claims Goldfeld’s conjecture for quadratic twists of every elliptic curve over ℚ: analytic ranks zero and one each occur with density one half, and the average analytic rank tends to one half. Combining the catalogue’s stated results yields a claimed full BSD formula for a density-one set of twists of each curve. Density one is an asymptotic counting statement; it still permits exceptional twists. Goldfeld paper
Hilbert’s tenth problem over the rationals
Family 004 claims that no algorithm can decide, for an arbitrary integer-coefficient polynomial with the number of variables included in the input, whether it has a rational zero. The rational-number case is the domain of the new claim. Rational Hilbert’s tenth paper
The proposed reduction constructs a sequence of finite rational-solvability tests for integer solvability. An integer zero should make every test succeed; if there is no integer zero, some test must fail. A hypothetical rational-solvability algorithm could then decide integer solvability by running two searches: enumerate integer witnesses and search for a failed rational test.
The arithmetic burden is proving that the tests have that exact separation property. The manuscript uses elliptic indices, local comparisons, valuations, height bounds and a compactness argument. Describing the two searches is the easy part; the long arithmetic construction is what must justify the claimed reduction. There is no family-004 Lean scope page in the inspected mapping.
Catalan’s constant is irrational
Family 005 claims that Catalan’s constant, G = 1 − 1/3² + 1/5² − 1/7² + …, cannot be written as a ratio of integers. This is a statement about a particular constant, not merely a guarantee that some member of a larger family of special values is irrational. Catalan paper
The paper assumes rationality and constructs mixed determinants whose entries involve G and other constants. Carefully chosen Taylor cancellations remove the unwanted ζ(2) terms. Rationality of G would then impose an arithmetic lower bound on the nonzero determinants, while an integral estimate supplies an incompatible upper bound. Controlling denominators and proving nonvanishing are both necessary; rapidly converging rational approximations alone would not suffice.
The family’s scope note identifies irrationality of G itself as the selected formal statement. Family 005 scope
The irrationality exponent of π is exactly two
Family 017 claims that for every exponent ν > 2, sufficiently large denominators q satisfy |π − p/q| ≥ q^(−ν), for every integer numerator p. This determines the irrationality exponent of π as two. π paper
It does not claim that π has bounded continued-fraction coefficients, or that one fixed positive constant c gives |π − p/q| ≥ c/q² for all denominators. The paper explicitly distinguishes these stronger conditions and says it does not provide an effective denominator threshold.
The proof roadmap uses weighted multivariable interpolation and nonzero determinants. It compares arithmetic denominator bounds with analytic estimates to rule out an unlimited supply of unusually accurate rational approximations. The reasoning summary shows the model testing its proposed interpolation argument against Liouville-type counterexamples and working through rank and nonvanishing difficulties.
The manuscript also claims convergence of the Flint–Hills series, Σ 1/(n³ sin²n), with angles measured in radians. The selected Comparator statement covers the exponent claim; the scope page places the series consequence outside that selected statement. The released solution entry point does contain a separate summability declaration. Selected verification scope and the contents of a source file should therefore be kept distinct. Family 017 scope
Ordinary two-point Chowla and corrected Elliott correlations
Family 007 concerns cancellation in correlations of multiplicative functions. One headline claim is an ordinary two-point Chowla bound for the Liouville function along fixed nonproportional affine forms, with a logarithmic-power saving. Another is the corrected binary Elliott statement under a uniform nonpretentiousness hypothesis. Correlation paper
“Ordinary” matters. An ordinary average weights the integers evenly up to a cutoff; a logarithmic average weights them differently. A statement that holds at almost all scales also differs from one that holds at every sufficiently large scale. The released reasoning summary repeatedly checks those distinctions.
The proposed method uses weighted divisor graphs, centered prime variables, nonbacktracking walks and spectral estimates. Its difficult steps include handling prime labels that occur only once and transferring independent-residue calculations to finite intervals. The scope page includes ordinary correlation statements and keeps the hypotheses on the multiplicative functions explicit. Family 007 scope
The Mahler conjectures, including equality cases
Family 087 claims both the symmetric and general geometric Mahler conjectures in every dimension. In the symmetric case, the asserted minimum volume product is 4ⁿ/n!, with equality characterized by Hanner bodies up to invertible linear transformation. In the general case, the asserted sharp bound is (n+1)^(n+1)/(n!)², with simplices as the equality cases. Family 087 scope
A polar body encodes the linear inequalities satisfied by a convex body. The volume product measures the sizes of the body and its polar together, in a way compatible with linear coordinate changes. Proving the sharp minimum requires an argument that works for all eligible bodies, rather than checking familiar examples.
The selected symmetric manuscript uses a conformal map, a holomorphic mass estimate and a Stokes calculation to obtain the lower bound. Its equality analysis leads to a ball-intersection property of normed spaces and a classification of Hanner bodies. The general-body reasoning summary develops a different cone, Gaussian and entropy-based route. Symmetric Mahler paper; Mahler reasoning summary
The scope page has a confusing transition: an early passage says the nonsymmetric result is not included, then a later passage supplies the general-body theorem and its Comparator link. Read it by individual linked statement. It lists symmetric inequality and equality targets, a general inequality and simplex-equality target, and a symplectic-width target. The functional inequalities advertised in the family are outside the selected geometric statements.
Unique Games and approximation hardness
Family 102 claims the Unique Games Conjecture and associated optimal approximation thresholds. Its selected Unique Games statement gives deterministic polynomial-time reductions from binary 3SAT with completeness arbitrarily close to one and soundness arbitrarily small, for fixed errors. The alphabet depends on those errors. Unique Games paper
In plain terms, the reduction converts satisfiable inputs into constraint games where almost every constraint can be met, and unsatisfiable inputs into games where very few can. Achieving both sides with the required quantifiers is the central difficulty.
The reasoning summary proposes quadratic gadgets, matrix-shortcode structure, decoding and gap amplification. It then discusses transferring hardness to basic semidefinite-programming thresholds for fixed finite constraint languages. These arguments build on existing PCP, expansion and rounding work; the release should not be read as inventing those foundations. Basic-SDP reasoning summary
The family’s scope page also lists Max-Cut, Vertex Cover, Min-UnCut and directed feedback vertex set targets. These hardness reductions do not prove P ≠ NP. They establish implications of the form “an approximation algorithm with this guarantee would give a polynomial-time algorithm for an NP-hard problem.” Family 102 scope
Arithmetic progressions and Erdős’s reciprocal-sum conjecture
Family 159 claims quasipolynomial bounds for finding arithmetic progressions of any fixed length in sufficiently dense sets. It also claims Erdős’s reciprocal-sum conjecture: every set of positive integers whose reciprocal sum diverges contains arithmetic progressions of every finite length. Progression paper
The proof roadmap follows a density-increment strategy. When a set has too few progressions, one seeks a structured region where its density increases. Repeating this cannot continue indefinitely, because density cannot exceed one. To obtain strong quantitative bounds, the cost of finding each new region must remain controlled.
The proposed construction uses triangular polynomial cells with a descending hierarchy of dimensions and precision. Its purpose is to prevent each new constraint from multiplying the complexity inherited from previous rounds. The reasoning summary spends considerable attention on that dependency order and on transferring estimates from sparse structured regions.
The selected family scope covers the reciprocal-sum consequence. It explicitly leaves the paper’s quantitative progression-free-set upper bound outside that selected statement. Family 159 scope
Counterexamples to Kaplansky conjectures
Families 196 and 197 claim counterexamples in group algebras. Family 196 constructs nonzero elements whose product is zero in the characteristic-two group algebra of a finitely presented torsion-free group. Family 197 claims a torsion-free characteristic-two example with ab = 1 but ba ≠ 1. Zero-divisor paper; Torsion-free direct-finiteness paper
These are negative resolutions: the claimed outcome is a counterexample to the conjecture, rather than a proof of its universal assertion. For direct finiteness, the algebraic certificate can include a nonzero c with ac = 0. If ba also equaled one, then c = b(ac) = 0, a contradiction.
The characteristic-two reasoning summary describes incidence-based constructions and a companion cellular-automaton implication. It takes a one-sided-inverse witness as input for that implication; the companion does not reconstruct the original witness. Direct-finiteness reasoning summary
There is also a scope mismatch worth recording. Family 197’s current catalogue headline includes the torsion-free strengthening, while its Lean scope page describes selected characteristic-two and odd-characteristic constructions involving torsion. The page’s title alone is insufficient to conclude that the torsion-free strengthening has been checked. Family 197 scope
Free group factors are claimed to be isomorphic
Family 287 claims L(ℱ₂) ≅ L(ℱ₃), resolving the free group factor isomorphism problem in the affirmative. The manuscript then uses established interpolation and amplification results to conclude that all interpolated free group factors, including the infinite parameter, are isomorphic. Free group factor paper
These objects are von Neumann algebras associated with free groups. The question concerns whether the resulting operator algebras retain enough information to distinguish the number of free generators.
The proposed construction makes small, trace-preserving perturbations to a generating tuple so that an additional generator can be recovered in the limit. The reasoning summary distinguishes norm convergence from generation of the whole von Neumann algebra, using a separate L²-density argument for the latter. Those limiting-generation and trace-preservation steps are the core burden of the claimed proof.
The selected scope covers normal trace-preserving isomorphisms across the interpolated parameters. The fundamental-group consequence is not a separate selected statement there. Family 287 scope
Spin glasses and the quantum Heisenberg ferromagnet
Family 221 claims the Mézard–Parisi hierarchical cavity formula for diluted even-arity Ising spin-glass models in the Panchenko–Talagrand class. Its assumptions include factorization, independence, integrability and positivity conditions. The selected scope asserts convergence of the pressure to an infimum over finite hierarchy depths and trial laws. Family 221 scope
The reasoning summary describes marked Poisson perturbations, tree identities, conditional decorrelation and a cavity lower comparison intended to match an interpolation upper bound. The physical intuition is a hierarchy of trial messages; the proof must show that the hierarchy captures the limiting pressure under the stated model assumptions. Spin-glass reasoning summary
Family 271 includes spontaneous magnetization for the nearest-neighbor isotropic quantum Heisenberg ferromagnet in every dimension d ≥ 3 and every positive integer or half-integer spin. Its selected scope constructs a translation-invariant zero-field equilibrium state at sufficiently low positive temperature with magnetization at least S/4. The family also contains stronger Bloch-law and correction claims. Family 271 scope
The magnetization reasoning uses an interchange/loop representation, pin tests, heat leakage estimates and a limiting equilibrium-state construction. The selected scope does not certify every temperature-asymptotic claim in the family. In particular, the October 5 finite-range Bloch-law paper should be assessed separately from the spontaneous-magnetization target. Heisenberg reasoning summary; Bloch-law paper
Global smoothness for relativistic Vlasov–Maxwell
Family 362 claims global existence and uniqueness for the three-dimensional, one-species relativistic Vlasov–Maxwell system with smooth admissible initial data. The particle density is compactly supported, while electromagnetic fields have finite energy and bounded derivatives of every order and satisfy the Gauss constraints. No smallness or symmetry condition is imposed. Vlasov–Maxwell paper
The system describes particles coupled to electromagnetic fields. A central obstacle is ruling out particle momenta becoming unbounded in finite time. The proposed proof controls signed momentum increments, keeping cancellations that would disappear if absolute values were taken too early. It then argues that successive momentum doublings require time intervals whose sum diverges, and invokes a bounded-momentum continuation theorem.
The reasoning summary identifies the difficult angular-occupation estimates, cutoff cancellations and regularity adjustments. It explicitly observes that the cited continuation theorem alone does not supply those new estimates. This is a useful map of what a specialist needs to check. The scope page selects global classical solvability under the stated hypotheses. Vlasov–Maxwell reasoning summary; Family 362 scope
More claims extend well beyond those headline examples
Other families include Artin primitive-root infinitude for every admissible integer base, Tingley’s sphere-isometry problem, sphere and three-manifold closed-geodesic results, and counterexamples involving Baum–Connes and Kadison–Kaplansky. The appendix provides the catalogue IDs and direct manuscript links for these and every other family.
Scope words remain decisive. Artin’s infinitude assertion is weaker than a full density formula. A counterexample with coefficients differs from one without coefficients. A result for every fixed progression length differs from a bound uniform in the length. Removing those qualifications would change the mathematics being reported.
Family 376 concerns universal computation in smooth, externally forced Navier–Stokes flows. Its construction claims to encode whether a machine halts in particle or velocity-field behavior. Such an engineered forcing result does not resolve the general three-dimensional Navier–Stokes existence and smoothness problem. Family 376 scope
How the model produced the results
OpenAI says the vast majority came from the same procedure using an unreleased internal model. It says existing mathematical evaluations had saturated, prompting expanded evaluation on open research problems. Some outputs build on earlier model-produced results. The release notes do not identify a public model name, parameter count, downloadable weights or reproducible inference endpoint.
The two stated exceptions are work on a zeta zero-free region and Hodge for CM abelian varieties. The alternate Re(s) > 11/12 zeta write-up was also human edited for readability. This establishes a disclosed human editorial contribution for that manuscript; it does not establish that every other paper received no human input.
The released reasoning summaries give a clearer picture of the mathematical work than the short procedure description. They show attempts to find counterexamples, comparisons with the literature, repairs to estimates, parameter-order checks and returns to earlier obstacles. They also show chained work: one attempt sometimes receives an earlier result as a premise, then develops an equality case, strengthening or consequence.
That dependency structure is crucial. If a principal result fails, a companion argument that assumes it may remain logically sound but lose its unconditional conclusion. Papers in one family should therefore be read as a dependency graph. Counting every consequence as a fresh, independent discovery exaggerates the evidence.
There are ten reasoning-summary PDFs, covering ten selected families. They total 202 pages in this snapshot, according to Kingy’s PDF page count. They are abridged summaries rather than full recorded model trajectories. Their visible text cannot recover all discarded branches, hidden reasoning, tool calls or inference retries. Their selection is not described as random, so they cannot establish a typical workflow for all 372 families.
The repeated self-checking in those summaries is useful evidence about the proposed arguments. It is not independent verification. A model returning to the same estimate many times can still retain the same false premise. Formal checking and specialist scrutiny address different parts of that risk.
What the Lean files do and do not establish
Lean expresses definitions, theorem statements and proofs in a language with machine-checkable inference. A successfully checked proof establishes the formal statement relative to the definitions and permitted axioms. Connecting that statement to the intended mathematics still requires inspecting the definitions, hypotheses and scope.
For this snapshot, Kingy counted 235 family scope pages in lean/docs/, all associated with catalogue families. That is about 63.2% of the 372 families. This is a count of documented associations with selected formalizations, not a measured proof-pass percentage. A family can contain several papers, and a selected theorem can cover only part of one paper.
The separate formalization.yaml manifest lists 162 source records and 185 main-result Comparator configurations. Its scope is “Partial progress.” Its review status is “unchecked.” These counts describe different layers of metadata; they should not be collapsed into one number of proved papers. The toolchain file specifies Lean 4.34.1. Formalization manifest
OpenAI’s verification instructions use Comparator. Its upstream documentation says that, under its stated trust assumptions, a successful run checks that a solution proves the challenge’s statement, stays within the permitted axioms and is accepted by the Lean kernel. The challenge file deliberately contains the target theorem with a placeholder proof; finding sorry in that target file is expected and does not by itself show that the proposed solution is incomplete. Comparator documentation
Kingy inspected ten selected Comparator JSON files and corresponding challenge statements, together with selected solution entry points. The configurations allow propext, Quot.sound and Classical.choice, and set enable_nanoda to false. That describes the supplied configurations. It is not evidence that these configurations passed, nor that every configuration in the repository has the same settings.
The responsible verification sequence is to inspect the target definitions and hypotheses, establish a trusted checking environment, run the selected Comparator configuration, and retain its output. Then compare the checked target with the manuscript’s principal theorem and advertised consequences. OpenAI recommends building small portions of its large library and documents a Linux memory-mapping issue for whole-library compilation. Release verification instructions
Kingy did not execute Lean, Comparator, an independent kernel or the full dependency build for this article. We also did not commission external referees. Accordingly, the article reports released claims and available artifacts, with selected static source inspection. It does not give the collection a mathematical correctness score.
How much compute did it use?
The disclosed unit is an average of three hours of ChatGPT Pro thinking compute per result with the internal model. The wording does not define it as three GPU-hours, three hours on one chip or exactly three elapsed hours for every individual paper.
A time-based inference budget leaves several questions unanswered. How much computation ran in parallel? Were unsuccessful candidates included in the average? How many attempts contributed to one retained result? Did the average include formalization, tool execution or only mathematical generation? What precisely is the denominator behind “result”? The release does not supply an accounting table that resolves those questions.
Even the obvious multiplication requires an assumption. If one equated “result” with a catalogue family, 372 × 3 would give 1,116 thinking-compute hours. If one instead used manuscripts, 722 × 3 would give 2,166. If three hours applied to every posed problem, approximately 4,000 × 3 would give approximately 12,000. These are conditional arithmetic illustrations, not reported totals. The paper/family distinction, fixed-procedure exceptions and failed-attempt accounting prevent selecting one as the project’s measured compute bill.
The model’s pretraining and post-training compute are another layer. A marginal inference budget for obtaining a result would not measure the research investment used to create the model. Formalization and checking can add separate computation, while human selection, editing and review add labor. None is quantified for this release.
| Resource or accounting field | Public disclosure in this snapshot |
|---|---|
| Model identity | Unreleased internal OpenAI model; no public model identifier |
| Average generation budget | Three hours of ChatGPT Pro thinking compute per result |
| Problems posed | Approximately 4,000 |
| Retained catalogue | 372 families; 722 manuscripts |
| Procedure exceptions | Zeta zero-free-region work; Hodge for CM abelian varieties |
| Aggregate inference dollar cost | Not disclosed |
| Input, output, cached and reasoning tokens | No evaluation usage ledger disclosed |
| Accelerator type, count and accelerator-hours | Not disclosed |
| FLOPs and electricity consumption | Not disclosed |
| Model training and post-training cost | Not disclosed |
| Failed attempts and retries | No separate resource account disclosed |
| Formalization and proof-check cost | Not disclosed |
| Human selection, editing and review labor | No labor-cost account disclosed |
How much did it cost, and how many tokens did it consume?
No defensible aggregate dollar figure can be calculated from the released information. Three hours of thinking compute is a duration measure. Converting it to money requires a price for that model and execution procedure, or an internal hardware-cost account. Neither is disclosed.
A monthly ChatGPT Pro subscription fee would not solve the problem. A subscription grants access subject to product terms; it is not an hourly rental of a specified accelerator configuration. The release’s use of the phrase “ChatGPT Pro thinking compute” also does not promise that a public subscriber can run this unreleased model or reproduce the result-generation procedure.
The repository does not supply a usage ledger of input, cached-input, output and reasoning tokens for the evaluation. A count of words in the manuscripts or released reasoning summaries would measure the documents, not the inference work. It would omit unsuccessful candidates and any reasoning excluded from the abridgment. Converting a visible transcript into a token estimate would therefore answer a different question.
For a priced API run, the basic accounting would multiply separately billed token categories by their applicable rates and add tool or infrastructure charges. For an internal run, costs might instead be allocated from hardware and operations. Both approaches require measurements absent here. Choosing the price of a familiar public model would add an unsupported assumption about the internal model’s identity and billing.
The same problem applies to energy and environmental estimates. Without accelerator types, utilization, total execution time and infrastructure information, an electricity figure would be speculation. The publication does not provide those ingredients.
The complete cost answer is therefore: average thinking-compute duration disclosed; total inference dollars, tokens, accelerator-hours, training cost, verification cost and human labor cost undisclosed in the inspected release material. That is an accountability gap worth recording, even if the mathematical results eventually survive scrutiny.
What this release tells us about AI research
The collection makes an ambitious claim about breadth. An internal model has produced proposed arguments in subjects ranging from Diophantine approximation to quantum statistical mechanics. The papers generally build on substantial human mathematics, and the formalization project imports existing Lean libraries. Any evaluation of the contribution should credit those foundations as well as examine the proposed new steps.
The strongest feature of the release is the availability of material that readers can inspect: full manuscripts, selected formal targets, proposed solution implementations, scope notes, pinned dependencies and reasoning summaries. That gives specialists concrete arguments to test, rather than a leaderboard score standing in for research achievement.
The missing information limits stronger conclusions. There is no complete table of the approximately 4,000 inputs and outcomes, no independent collection-wide correctness tally, no reproducible public model endpoint, and no detailed resource ledger. These omissions prevent claims about a verified solve rate, general autonomous-research reliability or cost per accepted theorem.
The practical next step is result-by-result scrutiny. A useful acceptance record would identify the manuscript version, exact statement checked, proof-check output, any scope exclusions, and independent mathematical review. A useful resource record would separate successful generation, failed attempts, formalization and checking. The release history will matter as corrections arrive.
Complete index of all 372 result families
The grouped index below preserves OpenAI’s catalogue IDs and titles. Each entry links to its first listed manuscript and records the number of associated manuscript links in the overview. A “Lean scope” link means OpenAI supplies a family scope page in this snapshot. It does not mean Kingy ran the proof or that every manuscript in that family is covered. Open the source catalogue for all companion papers and full statements.
Download the complete family and manuscript-link index (CSV). Catalogue titles and index metadata are adapted from OpenAI’s Apache-2.0 repository.
Number theory — 31 families
- 001. Milne's rationality conjecture
1 manuscript · No family scope page in this snapshot - 002. The full Birch–Swinnerton-Dyer formula in Selmer coranks zero and one
3 manuscripts · No family scope page in this snapshot - 003. The quasi-Riemann hypothesis
3 manuscripts · Lean scope - 004. Hilbert's tenth problem over ℚ
2 manuscripts · No family scope page in this snapshot - 005. Irrationality of Catalan's constant
1 manuscript · Lean scope - 006. Goldfeld's conjecture
2 manuscripts · No family scope page in this snapshot - 007. Two-point Chowla and the corrected binary Elliott conjecture
1 manuscript · Lean scope - 008. The Deligne–Drinfeld conjecture
1 manuscript · Lean scope - 009. Bogomolov–Pop and Milnor K-theoretic reconstruction
3 manuscripts · Lean scope - 010. Fontaine–Mazur modularity at the prime 2 and 2-adic pro-modularity
3 manuscripts · No family scope page in this snapshot - 011. The Ford–Konyagin–Luca conjecture on prime predecessors
3 manuscripts · No family scope page in this snapshot - 012. Independent largest prime factors of consecutive integers
1 manuscript · Lean scope - 013. Ostmann's inverse Goldbach conjecture
1 manuscript · Lean scope - 014. Restricted geometric Langlands, generic Ramanujan and Arthur parameters
8 manuscripts · No family scope page in this snapshot - 015. Torus-packet equidistribution in prime, quartic, and sextic degrees
3 manuscripts · Lean scope - 016. Zilber–Pink in abelian varieties and the Siegel threefold
4 manuscripts · No family scope page in this snapshot - 017. The irrationality exponent of π is 2
1 manuscript · Lean scope - 018. The Margulis–Platonov conjecture over global fields
2 manuscripts · No family scope page in this snapshot - 019. The p-adic section conjecture
2 manuscripts · No family scope page in this snapshot - 020. Squarefree quartics and power-free polynomial values
1 manuscript · Lean scope - 021. A quadratic bound for Jacobsthal's function
1 manuscript · Lean scope - 022. The weak inhomogeneous Duffin–Schaeffer conjecture
1 manuscript · No family scope page in this snapshot - 023. Patterson’s first moment for cubic Gauss sums
1 manuscript · Lean scope - 024. An asymptotic formula for the number of totients
1 manuscript · Lean scope - 025. Erdős’s short Egyptian-fraction conjecture
1 manuscript · Lean scope - 026. Positive lower density of large prime gaps
1 manuscript · Lean scope - 027. Integral density on curve character varieties
1 manuscript · No family scope page in this snapshot - 028. The Gaussian moat conjecture
1 manuscript · Lean scope - 029. Artin's primitive root conjecture: infinitude for every base
2 manuscripts · No family scope page in this snapshot - 030. Modularity over imaginary quadratic fields
1 manuscript · No family scope page in this snapshot - 031. Uchida's conjecture for open Galois homomorphisms
1 manuscript · No family scope page in this snapshot
Algebraic and complex geometry — 36 families
- 032. The rational Hodge conjecture for CM abelian varieties and products of K3 surfaces
8 manuscripts · No family scope page in this snapshot - 033. Campana's orbifold Iitaka conjecture and logarithmic subadditivity
5 manuscripts · Lean scope - 034. Log abundance and effective Iitaka fibrations
14 manuscripts · No family scope page in this snapshot - 035. Threefold log abundance in numerical dimension one in characteristic p>3
2 manuscripts · No family scope page in this snapshot - 036. Numerical semiampleness and generalized minimal models
4 manuscripts · No family scope page in this snapshot - 037. The sharp ordinary-double-point volume gap
2 manuscripts · No family scope page in this snapshot - 038. Fujita's freeness conjecture
1 manuscript · No family scope page in this snapshot - 039. Nagata's conjecture and maximal Seshadri constants
4 manuscripts · Lean scope - 040. Bloch's conjecture for complex surfaces
1 manuscript · No family scope page in this snapshot - 041. Hyperkähler SYZ and projective-space bases
2 manuscripts · No family scope page in this snapshot - 042. Oka classification for K3 surfaces and other compact complex surfaces
1 manuscript · No family scope page in this snapshot - 043. P=W for fixed-determinant moduli spaces
1 manuscript · No family scope page in this snapshot - 044. The equivariant cohomological Hikita conjecture for quivers
1 manuscript · No family scope page in this snapshot - 046. Counterexamples to Shafarevich holomorphic convexity
2 manuscripts · No family scope page in this snapshot - 047. Complex counterexamples to cancellation and affine fibrations
1 manuscript · Lean scope - 048. A characteristic-zero counterexample to Lipman–Zariski
1 manuscript · No family scope page in this snapshot - 049. A stable-coordinate counterexample in four variables
2 manuscripts · Lean scope - 050. A counterexample to Griffiths' positivity conjecture
1 manuscript · Lean scope - 051. Kobayashi's canonical-ampleness conjecture
1 manuscript · No family scope page in this snapshot - 052. Tangent-bundle splittings and universal covers
2 manuscripts · Lean scope - 053. A counterexample to Pixton's original completeness conjecture
1 manuscript · No family scope page in this snapshot - 054. Counterexamples to Kuznetsov's rationality conjecture
1 manuscript · No family scope page in this snapshot - 055. Toda's Gepner conjecture and large-volume stability
2 manuscripts · No family scope page in this snapshot - 056. Termination of fourfold minimal model programs
5 manuscripts · No family scope page in this snapshot - 057. Campana's abelianity conjecture and special varieties
3 manuscripts · No family scope page in this snapshot - 058. The Koll'ar–Pardon universal-cover conjecture
2 manuscripts · Lean scope - 059. Counterexamples to Zariski's multiplicity conjecture
2 manuscripts · No family scope page in this snapshot - 060. The Global Spherical Shell conjecture
1 manuscript · No family scope page in this snapshot - 062. The LeBrun–Salamon conjecture and projective contact classification
1 manuscript · No family scope page in this snapshot - 063. The generalized Mukai conjecture
1 manuscript · No family scope page in this snapshot - 064. The mu-constant problem for surface singularities
1 manuscript · No family scope page in this snapshot - 065. Virasoro constraints for complete intersections and projective bundles
2 manuscripts · No family scope page in this snapshot - 066. Bounded klt complements for Fano contractions
2 manuscripts · No family scope page in this snapshot - 067. The Campana–Peternell conjecture in dimension six
1 manuscript · No family scope page in this snapshot - 068. Anticanonical nonvanishing under smooth semipositivity
7 manuscripts · No family scope page in this snapshot - 069. Quantum geometric Langlands at irrational level
1 manuscript · No family scope page in this snapshot
Real and complex analysis — 16 families
- 071. Koebe's circle-domain conjecture and circle-domain rigidity
2 manuscripts · Lean scope - 072. Brennan's conjecture and a counterexample to Kraetzer's prediction
2 manuscripts · Lean scope - 073. The Falconer distance conjecture
1 manuscript · Lean scope - 074. Kakeya in three and four dimensions
2 manuscripts · No family scope page in this snapshot - 075. The Llog L Fourier-convergence conjecture
1 manuscript · No family scope page in this snapshot - 076. Ultraflat real Littlewood polynomials
3 manuscripts · Lean scope - 077. Fourier restriction for positively curved surfaces
2 manuscripts · No family scope page in this snapshot - 078. The three-dimensional Bochner–Riesz conjecture
1 manuscript · No family scope page in this snapshot - 079. Sogge's local smoothing conjecture in dimension three
1 manuscript · No family scope page in this snapshot - 080. The Sobolev endpoint in Carleson's Schrödinger convergence problem
2 manuscripts · No family scope page in this snapshot - 081. The David–Semmes Riesz-transform problem in higher codimension
1 manuscript · Lean scope - 082. Maximal and variational bounds for the triangular Hilbert transform
3 manuscripts · Lean scope - 083. Stein's conjecture for Hilbert transforms along Lipschitz directions
1 manuscript · Lean scope - 084. The geometric case of the Erdős similarity conjecture
2 manuscripts · Lean scope - 085. Endpoint regularity of the planar centered maximal function
1 manuscript · Lean scope - 086. An L^3 bound for the trilinear Hilbert transform
1 manuscript · No family scope page in this snapshot
Convex and metric geometry — 15 families
- 087. The Mahler conjectures and symplectic width
3 manuscripts · Lean scope - 088. Petty's projection-volume conjecture and simplex counterexamples
2 manuscripts · Lean scope - 089. Bounded-distortion L_1 embeddings of planar and bounded-treewidth graphs
2 manuscripts · Lean scope - 090. Universal optimality of the triangular lattice
4 manuscripts · Lean scope - 091. The logarithmic Brunn–Minkowski conjecture
1 manuscript · Lean scope - 092. The optimal order of convex-body covering density
2 manuscripts · Lean scope - 093. Dimension-free logarithmic Sobolev inequality for subgaussian log-concave measures
1 manuscript · No family scope page in this snapshot - 094. Subpolynomial dimension reduction in L_p
1 manuscript · Lean scope - 095. Hyperbolicity cones without semidefinite lifts
3 manuscripts · Lean scope - 096. The Gaussian propeller conjecture
1 manuscript · Lean scope - 097. The Euclidean Steinitz–Bergström conjecture
1 manuscript · Lean scope - 098. A negative answer to the Lang–Plaut problem
1 manuscript · Lean scope - 099. The sharp distortion of edit distance into ℓ_1
3 manuscripts · Lean scope - 100. A counterexample to Bang's cylinder-covering bound
4 manuscripts · Lean scope - 101. The sharp simplex conjecture for isotropic constants
1 manuscript · No family scope page in this snapshot
Theoretical computer science — 40 families
- 102. The Unique Games Conjecture and optimal approximation thresholds
5 manuscripts · Lean scope - 103. Derandomization of logarithmic space: mathsf L=mathsfRL=mathsfBPL
1 manuscript · No family scope page in this snapshot - 104. Quasipolynomial algorithms for mean-payoff, stochastic and parity games
4 manuscripts · Lean scope - 105. The 2-to-1 Games Conjecture with perfect completeness
1 manuscript · Lean scope - 106. Hardness of coloring three-colorable graphs
1 manuscript · Lean scope - 107. Matrix multiplication with exponent at most 9/4
3 manuscripts · Lean scope - 108. A cubic permanent–determinant lower bound
1 manuscript · Lean scope - 109. Integer multiplication below nlog n
1 manuscript · No family scope page in this snapshot - 110. Optimal-order randomized k-server on arbitrary metrics
2 manuscripts · Lean scope - 111. One-sample matroid prophet inequalities against an almighty adversary
1 manuscript · Lean scope - 112. Beyond the square-root exponent for depth-three circuits
1 manuscript · Lean scope - 113. Approximate counting and the perfect-matching entropy conjecture
2 manuscripts · Lean scope - 114. Approximate counting of common integer polymatroid bases
2 manuscripts · Lean scope - 115. Sampling and counting contingency tables with arbitrary margins
2 manuscripts · Lean scope - 116. Uniform identity testing for noncommutative formulas
3 manuscripts · Lean scope - 117. Uniform sparsest cut: hardness and semidefinite gaps
2 manuscripts · Lean scope - 118. Unbounded bin-packing gaps and the modified integer round-up conjecture
1 manuscript · Lean scope - 119. The Courtade–Kumar and Hellinger conjectures
2 manuscripts · Lean scope - 120. Almost-linear-time exact matching in general graphs
1 manuscript · No family scope page in this snapshot - 121. Almost-linear expected-time approximation of edit distance
1 manuscript · Lean scope - 122. Superpolynomial lower bounds and quasipolynomial reconstruction from deletion traces
3 manuscripts · Lean scope - 124. Polynomial-time scheduling on three identical machines
1 manuscript · Lean scope - 125. The approximation threshold for metric k-median
2 manuscripts · Lean scope - 126. Exponential semidefinite complexity of perfect matching
1 manuscript · Lean scope - 127. The asymptotic Gotsman–Linial conjecture
1 manuscript · Lean scope - 128. A factor-two approximation for shortest common superstring
1 manuscript · Lean scope - 129. Exponential state costs for two-way automata
2 manuscripts · Lean scope - 130. Fourier transforms below nlog n
2 manuscripts · Lean scope - 131. Polynomial mixing of graph switches with prescribed degrees
1 manuscript · Lean scope - 132. A counterexample to the quadratic sensitivity conjecture
1 manuscript · Lean scope - 133. The complexity of Weisfeiler–Leman refinement
4 manuscripts · Lean scope - 134. Generalized star height at most three
3 manuscripts · Lean scope - 135. Sharp homogeneous depth-five complexity of matrix products
1 manuscript · Lean scope - 136. The quasilinear PCP-for-PPAD conjecture
1 manuscript · No family scope page in this snapshot - 137. One-tape time simulation in two-fifths-power space
1 manuscript · No family scope page in this snapshot - 138. Subset Sum in O(2^0.49n) time
2 manuscripts · No family scope page in this snapshot - 139. Subpolynomial queries for log-concave sampling
1 manuscript · Lean scope - 140. Memory–sample lower bounds for noiseless Gaussian regression
6 manuscripts · Lean scope - 141. The existential theory of the reals and existential–universal sentences in the counting hierarchy
1 manuscript · No family scope page in this snapshot - 142. Deterministic polynomial factorization over prime fields
1 manuscript · No family scope page in this snapshot
Dynamical systems and ergodic theory — 12 families
- 143. Uniform limit-cycle bounds in Hilbert's sixteenth problem
2 manuscripts · Lean scope - 144. Banach's simple Lebesgue-spectrum problem
1 manuscript · Lean scope - 145. Rokhlin's multiple-mixing problem
1 manuscript · Lean scope - 146. Sinai's positive-entropy conjecture for the standard map
1 manuscript · Lean scope - 147. The near-boundary Birkhoff conjecture
2 manuscripts · No family scope page in this snapshot - 148. The dimension formula for self-similar measures on the line
1 manuscript · Lean scope - 149. Permanence for weakly reversible reaction networks
2 manuscripts · Lean scope - 150. Weak mixing of irrational triangular billiards
2 manuscripts · Lean scope - 151. A C^1 counterexample to Shub’s entropy conjecture
1 manuscript · Lean scope - 152. Zero entropy does not guarantee a smooth positive-volume model
1 manuscript · Lean scope - 153. Arithmetic classification of Bernoulli convolutions
1 manuscript · No family scope page in this snapshot - 154. Pointwise multiple ergodic averages for mixing transformations
4 manuscripts · No family scope page in this snapshot
Combinatorics — 37 families
- 155. A counterexample to periodic tiling in dimension three
1 manuscript · Lean scope - 156. Borsuk's conjecture fails in dimension nine
1 manuscript · Lean scope - 157. Counterexamples to the Hadwiger and Colin de Verdi`ere conjectures
3 manuscripts · Lean scope - 158. The Euclidean plane cannot be colored with five colors
1 manuscript · Lean scope - 159. Erdős's reciprocal-sum conjecture and quasipolynomial Szemerédi bounds
1 manuscript · Lean scope - 160. Superexponential van der Waerden numbers
1 manuscript · Lean scope - 161. Counterexamples to Sidorenko's conjecture and the forcing conjecture
1 manuscript · Lean scope - 162. Counterexamples to Ryser's covering and Gy'arf'as's tree-cover conjectures
2 manuscripts · Lean scope - 164. Hindman's finite sums and products conjecture
1 manuscript · No family scope page in this snapshot - 165. Exact crossing numbers of complete and complete bipartite graphs
2 manuscripts · Lean scope - 166. The higher-dimensional Erdős distinct-distances conjecture
1 manuscript · No family scope page in this snapshot - 167. Pinned distances and a power saving for planar unit distances
2 manuscripts · Lean scope - 168. Combinatorial invariance of Kazhdan–Lusztig polynomials
1 manuscript · Lean scope - 169. The Shareshian–Wachs e-positivity conjecture
1 manuscript · Lean scope - 170. Sharp logarithmic exponents for off-diagonal Ramsey numbers
2 manuscripts · Lean scope - 171. The hypercube Ramsey conjecture
1 manuscript · No family scope page in this snapshot - 172. Classification of finite Euclidean Ramsey configurations
1 manuscript · Lean scope - 173. Seymour's second-neighborhood conjecture
1 manuscript · Lean scope - 174. Deterministic construction of strong thin spanning trees
2 manuscripts · Lean scope - 175. Talagrand's conjectures and graph decompositions at expectation thresholds
3 manuscripts · Lean scope - 176. The second Kahn–Kalai conjecture
1 manuscript · Lean scope - 177. Bounded-degree coboundary expanders in every dimension
1 manuscript · Lean scope - 178. Deterministic nonbipartite Ramanujan graphs in every fixed degree
1 manuscript · No family scope page in this snapshot - 179. The circulant Hadamard conjecture
1 manuscript · Lean scope - 180. Barnette's Hamiltonian-cycle conjecture
1 manuscript · Lean scope - 181. The Erdős–Gallai cycle-decomposition conjecture
1 manuscript · Lean scope - 182. Power savings for polynomial-difference-free sets
3 manuscripts · Lean scope - 183. Power savings for planar halving lines and k-sets
1 manuscript · Lean scope - 184. Coloring and independence in graphs with forbidden subgraphs
2 manuscripts · Lean scope - 185. Counterexamples to infinite matroid intersection and packing/covering
1 manuscript · Lean scope - 186. The Friedgut–Kalai graph and hypergraph threshold conjectures
2 manuscripts · Lean scope - 187. Snaky in 21 Maker moves
1 manuscript · Lean scope - 188. The sharp constant in random triangle removal
1 manuscript · Lean scope - 189. Exact cycle–clique Ramsey numbers
1 manuscript · Lean scope - 190. Polynomial removal fails for ordered binary matrices
1 manuscript · Lean scope - 191. A power improvement in the Heilbronn triangle problem
1 manuscript · Lean scope - 192. A counterexample to the Gopalan–Servedio conjecture
1 manuscript · Lean scope
Algebra — 18 families
- 193. Serre's intersection-multiplicity conjecture
1 manuscript · No family scope page in this snapshot - 194. Lech's multiplicity conjecture
1 manuscript · Lean scope - 195. A counterexample to the small Cohen–Macaulay module conjecture
1 manuscript · No family scope page in this snapshot - 196. A counterexample to Kaplansky's zero-divisor conjecture
1 manuscript · Lean scope - 197. Nonsofic groups and group-ring counterexamples
4 manuscripts · Lean scope - 198. A counterexample to the little finitistic-dimension conjecture
1 manuscript · Lean scope - 199. Counterexamples to conjectures of Auslander–Reiten, Tachikawa, and Nakayama
2 manuscripts · Lean scope - 200. Eisenbud–Green–Harris and lex-plus-powers in characteristic zero
2 manuscripts · No family scope page in this snapshot - 201. A counterexample to Kurosh's division-ring problem
1 manuscript · No family scope page in this snapshot - 202. The blockwise Alperin weight conjecture
1 manuscript · No family scope page in this snapshot - 203. Donovan's conjecture over fields and discrete valuation rings
2 manuscripts · No family scope page in this snapshot - 204. Tensor saturation for even spin groups
1 manuscript · No family scope page in this snapshot - 205. Saxl's conjecture and universal tensor squares
2 manuscripts · Lean scope - 206. Finite lattice representation: counterexamples and undecidability
2 manuscripts · Lean scope - 207. The ℓ^1-Bass and complex Bass trace conjectures
2 manuscripts · Lean scope - 208. The finite Benson–Etingof–Ostrik conjecture
1 manuscript · No family scope page in this snapshot - 209. Integral counterexamples to Gersten’s conjecture
2 manuscripts · No family scope page in this snapshot - 210. Foulkes’ conjecture for sixth powers and quadratic stabilization
2 manuscripts · Lean scope
Probability and statistical mechanics — 29 families
- 211. Geometry, diffusion, and spectra of random planar maps
7 manuscripts · Lean scope - 212. No bigeodesics and smooth limit shapes in planar first-passage percolation
2 manuscripts · Lean scope - 213. No infinite critical clusters on quasi-transitive graphs
2 manuscripts · Lean scope - 214. The Benjamini–Schramm nonuniqueness conjecture
1 manuscript · Lean scope - 215. Massive continuum limits and exact mass asymptotics for planar O(n) models
5 manuscripts · Lean scope - 216. Critical logarithmic corrections and BKT scaling for the planar XY model
6 manuscripts · No family scope page in this snapshot - 217. The low-temperature Sherrington–Kirkpatrick fluctuation law
2 manuscripts · No family scope page in this snapshot - 218. Conformal universality for weakly interacting and disordered Ising models
6 manuscripts · Lean scope - 219. GOE universality for random regular graphs with weak disorder
2 manuscripts · No family scope page in this snapshot - 220. Directional zero–one laws and ballisticity in random environments
3 manuscripts · Lean scope - 221. The Mézard–Parisi formula for diluted spin glasses
1 manuscript · Lean scope - 222. Perceptron free energies and microscopic jamming
4 manuscripts · Lean scope - 223. Conformal limits of square-lattice random-cluster interfaces
6 manuscripts · No family scope page in this snapshot - 224. Critical and near-critical universality for Voronoi percolation
3 manuscripts · No family scope page in this snapshot - 225. Gaussian free field limits for the balanced six-vertex model
1 manuscript · No family scope page in this snapshot - 226. The double-dimer CLE_4 conjecture in the half-plane
1 manuscript · No family scope page in this snapshot - 227. The dynamical phase transition in the Sherrington–Kirkpatrick model
8 manuscripts · Lean scope - 228. Continuum phase transitions for radial pair potentials
2 manuscripts · Lean scope - 229. Sharp three- and four-state reconstruction thresholds
3 manuscripts · Lean scope - 230. Exact Hausdorff measure for SLE
2 manuscripts · Lean scope - 231. The free uniform spanning forest is a factor of IID
1 manuscript · Lean scope - 232. Gaussian fields and SLE interfaces for Lipschitz heights
3 manuscripts · No family scope page in this snapshot - 233. The joint critical Ashkin–Teller scaling limit
1 manuscript · No family scope page in this snapshot - 234. All-temperature pressure for orthogonally invariant Ising spin glasses
1 manuscript · Lean scope - 235. Random-SAT thresholds, sharp variance and computability
4 manuscripts · Lean scope - 236. The factor-of-IID threshold for free Ising states on trees
1 manuscript · Lean scope - 237. The three-quarter diameter exponent for honeycomb walks
13 manuscripts · Lean scope - 238. Optimal logarithmic mixing of the Thorp shuffle
12 manuscripts · Lean scope - 239. Sharp singularity rates for symmetric sign matrices
2 manuscripts · No family scope page in this snapshot
Mathematical logic — 6 families
- 240. Shelah's eventual categoricity conjecture
2 manuscripts · Lean scope - 241. Rigidity of the Turing degrees
1 manuscript · Lean scope - 242. Single-fold Diophantine representations
1 manuscript · Lean scope - 243. Choiceless counting does not capture polynomial time
2 manuscripts · Lean scope - 244. The partition principle does not imply choice
1 manuscript · Lean scope - 245. The β-Barendregt–Geuvers–Klop conjecture
1 manuscript · Lean scope
Group theory — 14 families
- 246. Cannon's conjecture
1 manuscript · Lean scope - 247. An infinite finitely presented residually finite 2-group
2 manuscripts · Lean scope - 248. Thompson's group F is nonamenable
1 manuscript · Lean scope - 249. A finitely generated counterexample to Eilenberg–Ganea
1 manuscript · Lean scope - 250. The Boone–Higman conjecture and higher finiteness
3 manuscripts · Lean scope - 251. Amenability, unitarizability, and Ulam stability
2 manuscripts · Lean scope - 252. A non-residually-finite torsion-free hyperbolic group
1 manuscript · Lean scope - 253. An infinite finitely presented simple amenable group
1 manuscript · Lean scope - 254. Classifying spaces and geometric obstructions for Artin groups
3 manuscripts · Lean scope - 255. Quasi-isometric rigidity of virtually polycyclic groups
1 manuscript · Lean scope - 256. Howie's conjecture on equations over groups
2 manuscripts · Lean scope - 257. A hyperbolic group with no geometric CAT(0) action
1 manuscript · Lean scope - 258. Gersten's conjecture for one-relator groups
2 manuscripts · No family scope page in this snapshot - 259. A group without fixed price
1 manuscript · No family scope page in this snapshot
Mathematical physics — 25 families
- 260. Spacetime Penrose inequalities and rigidity
13 manuscripts · Lean scope - 261. Localization and delocalization in the Anderson model
2 manuscripts · Lean scope - 262. Sharp one-dimensional Lieb–Thirring inequalities
3 manuscripts · Lean scope - 263. The ionization and generalized ionization conjectures
3 manuscripts · Lean scope - 264. Strong cosmic censorship near two-ended Kerr data
3 manuscripts · No family scope page in this snapshot - 265. The two-dimensional gapped area law
2 manuscripts · No family scope page in this snapshot - 266. Exactly three mutually unbiased bases in dimension six
2 manuscripts · Lean scope - 267. Positive-temperature Bose–Einstein condensation and quantum depletion
5 manuscripts · Lean scope - 268. The spin-one Haldane gap
2 manuscripts · No family scope page in this snapshot - 269. The Laughlin gap and stability under scalar disorder
2 manuscripts · Lean scope - 270. Threshold and positive-energy bound states of the BFSS model
2 manuscripts · No family scope page in this snapshot - 271. Bloch's law and spontaneous ferromagnetic order
4 manuscripts · Lean scope - 272. Entanglement without secret key and the PPT-square conjecture
1 manuscript · Lean scope - 273. The entropy photon-number inequality
1 manuscript · Lean scope - 274. Moore's parity conjecture for QAC^0
2 manuscripts · Lean scope - 275. QMA-hardness of continuum Coulomb energy
2 manuscripts · Lean scope - 276. The classical capacity of generalized amplitude damping
1 manuscript · Lean scope - 277. Threshold repetition for entangled games
1 manuscript · Lean scope - 278. Failure of Kohn–Sham ensemble representation
1 manuscript · No family scope page in this snapshot - 279. Exact quantum factoring over a fixed finite gate set
1 manuscript · Lean scope - 280. Strong locality for strongly rational unitary vertex operator algebras
1 manuscript · Lean scope - 281. QAOA optimality for the SK model
2 manuscripts · Lean scope - 282. Scale-to-conformal enhancement in four-dimensional QFT
1 manuscript · No family scope page in this snapshot - 283. Polynomial-time, constant-error unitary synthesis from a Boolean oracle
1 manuscript · No family scope page in this snapshot - 284. The optimal randomized–quantum query exponent
1 manuscript · No family scope page in this snapshot
Operator algebras — 19 families
- 285. Counterexamples to Baum–Connes and Kadison–Kaplansky
3 manuscripts · No family scope page in this snapshot - 286. Arithmetic rigidity of lattice von Neumann algebras
2 manuscripts · No family scope page in this snapshot - 287. All nonabelian free group factors are isomorphic
1 manuscript · Lean scope - 288. Kadison's similarity conjecture
1 manuscript · Lean scope - 289. The strong Kadison–Kastler conjecture
3 manuscripts · Lean scope - 290. Connes' bicentralizer conjecture and relative bicentralizers
2 manuscripts · Lean scope - 291. Toms–Winter and equivariant Jiang–Su stability
4 manuscripts · Lean scope - 292. A counterexample to Kirchberg's norm-ultrapower embedding problem
1 manuscript · Lean scope - 293. A counterexample to the hyperinvariant-subspace problem
2 manuscripts · Lean scope - 294. A counterexample to Kaplansky's quasitrace conjecture
1 manuscript · Lean scope - 295. The Kadison–Ringrose cohomology conjecture
1 manuscript · Lean scope - 296. The generator problem for finite factors
1 manuscript · Lean scope - 297. A ZFC counterexample to Naimark's problem
1 manuscript · Lean scope - 298. A counterexample to Voiculescu’s free-entropy equality conjecture
1 manuscript · Lean scope - 299. The Kirchberg–Ro rdam character criterion
1 manuscript · Lean scope - 300. The Popa–Vaes quadratic strong-operator paving conjecture
2 manuscripts · No family scope page in this snapshot - 301. Classification by trace cones after Razak–Jacelon stabilization
1 manuscript · No family scope page in this snapshot - 302. The Phillips–Toms formula for minimal integer actions
2 manuscripts · No family scope page in this snapshot - 303. From ordinary to strong pure infiniteness
1 manuscript · Lean scope
Topology — 18 families
- 304. The Hilbert–Smith conjecture in every dimension
1 manuscript · No family scope page in this snapshot - 305. Counterexamples to disk embedding and Wall's manifold conjecture
3 manuscripts · No family scope page in this snapshot - 306. The purely cosmetic surgery conjecture for knots in S^3
1 manuscript · No family scope page in this snapshot - 307. Failure of rational injectivity for maximal coarse assembly
2 manuscripts · Lean scope - 308. Smith–Toda complexes at every height with varying primes
2 manuscripts · No family scope page in this snapshot - 309. The Kervaire invariant problem at the prime three
1 manuscript · No family scope page in this snapshot - 310. Quillen's conjecture in rational homology
1 manuscript · No family scope page in this snapshot - 311. Chai's invariant-ideal conjecture
1 manuscript · No family scope page in this snapshot - 312. The Grothendieck homotopy hypothesis
1 manuscript · Lean scope - 313. Finite generation for the K(n)-local sphere
1 manuscript · No family scope page in this snapshot - 314. The chromatic Smith fixed-point problem for finite p-groups
1 manuscript · No family scope page in this snapshot - 315. The four-dimensional Singer conjecture
1 manuscript · No family scope page in this snapshot - 316. Curtis’s conjecture
1 manuscript · No family scope page in this snapshot - 317. Thomason model structures in every strict higher dimension
1 manuscript · Lean scope - 318. Chromatic splitting: counterexamples and filtrations
5 manuscripts · No family scope page in this snapshot - 319. Counterexamples to the Hahn–Wilson conjecture at height two
1 manuscript · No family scope page in this snapshot - 320. A four-dimensional counterexample to Borel rigidity
1 manuscript · No family scope page in this snapshot - 321. A counterexample to Wall's finite D(2) conjecture
1 manuscript · No family scope page in this snapshot
Functional analysis — 11 families
- 322. Tingley's sphere-isometry problem
1 manuscript · Lean scope - 323. Relative independence of the separable quotient problem
1 manuscript · Lean scope - 324. Lipschitz equivalence without linear isomorphism
2 manuscripts · Lean scope - 325. The complete Crouzeix conjecture
2 manuscripts · Lean scope - 326. The cotype–cotype conjecture under the approximation property
1 manuscript · Lean scope - 327. Markov type characterizes superreflexivity
1 manuscript · Lean scope - 328. Fixed points of nonexpansive maps in reflexive Banach spaces
1 manuscript · Lean scope - 329. A counterexample to Pietsch's metric-entropy duality conjecture
1 manuscript · Lean scope - 330. A negative answer to Kalton's Lipschitz-free approximation question
1 manuscript · Lean scope - 331. Asymptotic midpoint uniform convexity without asymptotically uniformly convex renorming
7 manuscripts · Lean scope - 332. Metric Markov cotype two for ℓ_1
1 manuscript · No family scope page in this snapshot
Differential geometry — 29 families
- 333. Smooth isometric immersions of surfaces into ℝ^4
1 manuscript · Lean scope - 334. A smooth surface metric with no local immersion in ℝ^3
1 manuscript · Lean scope - 335. Gromov's integral scalar-curvature inequality
2 manuscripts · No family scope page in this snapshot - 336. Spectral scalar curvature and codimension-two width
3 manuscripts · No family scope page in this snapshot - 337. Cartan–Hadamard isoperimetry and CAT(0) fillings
2 manuscripts · Lean scope - 338. Yau's uniformization conjecture
1 manuscript · No family scope page in this snapshot - 339. Katok's entropy rigidity conjecture
1 manuscript · No family scope page in this snapshot - 340. A counterexample to the nearby Lagrangian conjecture
1 manuscript · No family scope page in this snapshot - 341. Donaldson's hypersymplectic deformation conjecture
1 manuscript · No family scope page in this snapshot - 342. Donaldson's tamed-to-compatible conjecture
1 manuscript · Lean scope - 343. Sharp symplectic ball-packing criteria in higher dimensions
1 manuscript · Lean scope - 344. The metric Blaschke conjecture
1 manuscript · No family scope page in this snapshot - 345. Infinitely many closed geodesics on spheres and three-manifolds
1 manuscript · No family scope page in this snapshot - 346. Sharp singular-set bounds for stationary integral varifolds
2 manuscripts · No family scope page in this snapshot - 347. Counterexamples to strong forms of Arnold's fixed-point conjecture
5 manuscripts · Lean scope - 348. Nonnegatively curved Einstein four-manifolds and a topological gap
3 manuscripts · Lean scope - 349. The Solomon–Yau least-volume conjecture
1 manuscript · No family scope page in this snapshot - 350. Yau's nodal conjecture: surfaces and counterexamples
3 manuscripts · Lean scope - 351. Scalar curvature detects four-dimensional Ricci-flow singularities
3 manuscripts · No family scope page in this snapshot - 352. Finite-time singularity of Calabi flow
1 manuscript · No family scope page in this snapshot - 353. The sharp dimension threshold for affine Bernstein rigidity
2 manuscripts · Lean scope - 354. Isoperimetric regions in the cubic three-torus
1 manuscript · Lean scope - 355. Unique tangent flows at the first surface singularity
1 manuscript · No family scope page in this snapshot - 356. Gigli's characterization of Alexandrov curvature
2 manuscripts · Lean scope - 357. Bi-Lipschitz coordinates at every regular RCD point
1 manuscript · No family scope page in this snapshot - 358. A three-manifold with no conjugate points and no nonpositively curved metric
1 manuscript · Lean scope - 359. Negative Kähler curvature without bounded holomorphic coordinates
2 manuscripts · Lean scope - 360. Villani’s convexity conjecture and regular optimal transport
2 manuscripts · Lean scope - 361. Counterexamples to Yau's harmonic dimension bound
2 manuscripts · Lean scope
Partial differential equations — 16 families
- 362. Global smoothness for relativistic Vlasov–Maxwell
1 manuscript · Lean scope - 363. Boltzmann nonuniqueness with exact local conservation
2 manuscripts · Lean scope - 364. Kinetic limits and fluctuations over the Boltzmann lifespan
2 manuscripts · No family scope page in this snapshot - 365. Joint metric and connection recovery from one boundary patch
3 manuscripts · Lean scope - 366. The planar Mumford–Shah regularity conjecture
1 manuscript · No family scope page in this snapshot - 367. The critical dimension for the one-phase Bernoulli problem
1 manuscript · Lean scope - 368. The three-dimensional Ball–Evans approximation problem
2 manuscripts · No family scope page in this snapshot - 369. The hot spots conjecture for simply connected planar domains
1 manuscript · Lean scope - 370. The subcritical Lane–Emden and Hénon–Lane–Emden conjectures
1 manuscript · Lean scope - 371. Stable blowup for a defocusing Schrödinger equation
1 manuscript · Lean scope - 372. Global uniqueness in smooth isotropic elasticity
1 manuscript · Lean scope - 373. Nonattainment in three-marginal Coulomb transport
1 manuscript · Lean scope - 374. Sharp one-third stability of optimal transport maps
1 manuscript · Lean scope - 375. De Giorgi's conjecture in dimension eight
1 manuscript · No family scope page in this snapshot - 376. Universal computation in forced Navier–Stokes flows
9 manuscripts · Lean scope - 377. Interior C^1,α regularity for infinity-harmonic functions
1 manuscript · No family scope page in this snapshot
Sources and reporting method
This report is anchored to OpenAI repository commit adc7f1241b42e322a6451854ab7e4b4c146bf78a, whose commit timestamp is October 6, 2026 at 21:58:50 UTC. The catalogue itself is dated October 6. Pinned source links preserve the version examined; the live repository can contain later corrections.
Kingy parsed the complete overview and manuscript map, checked the preprint-directory listing, downloaded 21 selected manuscript PDFs and all ten reasoning-summary PDFs, and examined introductions, principal claims, proof roadmaps, selected reasoning passages, the 235 family scope-page associations for indexing, and selected scope documents in detail. We counted records in the formalization manifest and inspected ten selected Comparator configurations, their challenge statements and selected solution entry points. Reading or indexing artifacts is distinct from executing their mathematical verification.
The article uses Clay Mathematics Institute descriptions to explain the scope of the Riemann, Hodge and BSD problems, and the Comparator project’s own documentation to explain what a successful check would establish. It does not infer theorem acceptance from star counts, social posts or the presence of a PDF. Numerical calculations and catalogue counts are Kingy’s analysis and are labeled as such.
OpenAI’s repository is released under Apache 2.0. The family titles and index metadata above are adapted from its catalogue with attribution to OpenAI. Mathematical summaries are reporting on the source claims, rather than independent certificates of correctness. Repository license
Trending on Kingy
Keep reading with the stories getting the most attention now.
The Kingy Brief
Get The Kingy Brief.
Every Friday: the AI launches worth your time, what we actually tested, and one thing to try. Free. Unsubscribe anytime.
Free · Double opt-in · Unsubscribe anytime