Primary Sources: AI Contributions to Mathematics

This is one of four source documents for AI’s Contribution to Discovery. The four source documents are cyber, math, algorithms and optimization, and cross-cutting evidence, models, and method.

The conventions this document follows — what an entry must contain, the status vocabulary, the standing rules, and the eight questions entries are tagged against — are set out in the method and cross-cutting document.

Overview

This overview reads the document against the two questions the argument asks of every domain: how large is the flow of AI-contributed results next to the human flow, and has any curve of mathematical discovery changed slope since agents arrived. Two keystone figures collect what the log can measure. The first is bound and record series — numbers that tighten over time. The second is open-problem lists — binary falls and catalogue stocks. Every plotted quantity is a record of collective progress rather than a model capability score, because a capability score has no pre-AI history and so cannot show a bend.

Bound / record series

The math evidence on the two overview questions: AI-attributed stocks, targeted rates, and record steps where comparison is possible (top row), and the long-run exponent records that show no change of slope (bottom row).

Panel 1 plots the Erdős problems database’s own site snapshots — problems catalogued, problems recorded as solved, and statements formalized in Lean — with the months after the catalogue count stopped changing shaded, since only there can a rise in solved status no longer be caused by adding already-solved historical problems; the red point is the cumulative count of problems the project’s AI-contributions wiki records as fully resolved by AI with non-significant human involvement, frozen 2026-06-30 [→ Erdős wiki]. The cohort and statuses remain editable, and status-change dates need not equal solution dates. Panels 2–4 draw three of the record sequences with a dated AI step from the AlphaEvolve baseline this log assembled — a pre-committed twelve-problem sample transcribed from the paper, extended on 2026-07-28 to every record-status problem in the frame: the two quantities on which AI and human steps genuinely contested a record, and a third whose whole history is a 1996 construction and a 2025 AlphaEvolve improvement [→ record steps]. Panels 5–8 ask the exponent database for the best bound derivable from the literature of each year — one slice from each of the three families \(\mu\), \(A\) and \(\beta\), plus a second \(\mu\) slice that kept improving until 2023 — so they are curves of available knowledge rather than of published claims [→ ANTEDB rates]. The source supplies the total, solved-status, and Lean-formalization counts in panel 1; only the comparison to the wiki’s roughly thirteen AI-standalone resolutions is this log’s arithmetic.

Lists of open problems

Five scored fall-track lists and a full-width Erdős catalogue-stock panel; Scottish Book omitted.

Prestige fall tracks barely move through the highlighted 2026 period, but they are no longer a pure zero for AI: Smale 16 falls in 2026 to an independently checked Alpöge–Claude Fable counterexample, while Millennium remains 1/7 (Perelman 2003), Landau 0/4, and Hilbert ends its consensus-resolved rows with Hales 1998. TOPP marks 17 of 78 entries solved, settled, or closed on its own status lines. The Erdős panel is a changing catalogue stock, not a solution-date series. The Scottish Book is named among the prestige lists but omitted from the figure for want of a current fall ledger. Scoring rules, source caveats, and the mixed GitHub/website tip of the Erdős series are in the ledger entry [→ famous open-problem lists].

The size of the flow. The Erdős counts establish that AI-standalone resolutions remain a small part of the recorded solved stock, not that they are a small share of current human flow. The database records 565 of 1,217 catalogued problems with solved status as of 8 August 2026, while its AI-contributions wiki, frozen 30 June, attributes roughly 47 contributions to AI standalone — about 13 full resolutions, 25 partial, and 9 incorrect [→ Erdős wiki]. The dates and attribution categories differ, so subtracting 13 from 565 does not estimate human output. Tao’s rough arithmetic supplies useful scale but not a rate: “Fifty-odd problems have been solved with AI assistance, which is great, but there’s like six hundred to go” [→ Tao]. The one rate with a real denominator is AlphaProof Nexus, which, pointed at 353 open Erdős problems, resolved 9 autonomously — about 2.5%, at a few hundred dollars each — and proved 44 of 492 OEIS conjectures, about 9%, on a more mechanically stated corpus [→ AlphaProof Nexus]. Where AI and human record steps can be compared on the same quantity, the AI steps are ordinary in size — a median of about +0.9% against about +2.8% for human work by hand and +2.5% for human computer search — with the caveat that the head-to-head exists for only two quantities, because six of the twelve sampled problems yielded no scalar record sequence at all [→ record steps]. Humans have also promptly retaken AI records on some quantities: on the sums-and-differences bound within months, in a paper titled “improvement over AlphaEvolve,” while on the 11-dimensional kissing number the human response was best-in-other-dimensions rather than a retake of AlphaEvolve’s 593, after which collective agents pushed the same bound to 604 [→ kissing number]. The flow is not all shallow — the unit-distance disproof was judged a major result by outside experts, on a problem worked for eighty years [→ unit-distance] — but so far it is one such result.

The prestige lists have barely moved, but the zero is gone. The open-problems keystone above is the ceiling check: Hilbert, Landau, Smale, the Scottish Book, and the Millennium Prize Problems are what the public means by open mathematics, and through mid-2026 only Smale records an AI-attributed fall — the July Alpöge–Claude Fable counterexample to the Jacobian conjecture in dimension 3 (hence every dimension at least 3), with independent Lean and Isabelle checks of the determinant and collision. The two-dimensional case remains open. Prestige lists are selected against cheap verification, so their near-zero is almost uninformative about general capability, but that Smale fall shows an easily checked counterexample can still register there [→ famous open-problem lists].

A change of slope. The century-scale series are flat through the highlighted 2026 period. The Lindelöf exponent \(\mu(1/2)\) fell from \(5/28\) to \(13/84\) across fifteen improvements between 1920 and 2017 — a factor of 0.87 in a century, an implied halving time near 500 years — and nothing has happened to it since. That is not because AI failed on it quietly: no AI has been applied to it, the database’s authors describe AI integration as a future possibility they have not pursued, and when AlphaEvolve was pointed at analytic number theory it “struggled to take advantage of the number theoretic structure in the problem, even when given suitable expert hints” [→ ANTEDB, AlphaEvolve mathematics]. The one recent bend in these records — the zero-density exponent at 3/4, flat for 84 years after Ingham — was made by Guth and Maynard in 2024, by hand. The other slices tell the same story: \(\mu(3/5)\) improved seventeen times between 1920 and 2023, the last two steps by Bourgain in 2017 and Trudgian and Yang in 2023, and \(\beta(1/10)\), whose first derivable bound dates only from 1993, has not moved since 2017 — every step in these records is human work. Where AI does enter a series it arrives as a burst inside an old trend rather than as a new slope: four steps in 2025, two of them AlphaEvolve’s, on a bound whose previous four steps came in 2007. Every dated AI result in this document falls between December 2023 and August 2026, so any bend the AI flow will put in a discovery curve is at most about two and a half years old. And the Erdős solve count, the one corpus-level flow AI demonstrably feeds, has eleven months of measurable history — too short to carry a before-and-after comparison. The series that do rise steeply through this period are competition and benchmark scores — IMO silver under multi-day compute in 2024, gold within the contest time limit in 2025, FrontierMath from under 2% to 46–88% on its hardest tier [→ AlphaProof and IMO 2024, IMO 2025, FrontierMath] — but these begin near the models’ arrival and measure model scores rather than the stock of mathematics, so they cannot show whether the discovery curve bent, and the log records independent reasons not to chain FrontierMath’s versions into a single series.

Snapshot of the measurable objects this document uses. Status is about slope change and LLM contribution. Astra rows (Aug 2026) are vendor claims with Lean certificates; peer review pending.

Bound / record series.

Series	What it is	Status
Analytic number theory exponents (ANTEDB)	Best known values of classical exponents (\(\mu\), zero-density \(A\), \(\beta\), …) as functions of a parameter, with dated literature behind each.	No slope change through 2026; no LLM contribution (AlphaEvolve “struggled” even with hints). Last bends human (e.g. Guth–Maynard 2024). Non-LLM collation/search over the relation database did improve some bounds at launch — not an LLM effect.
Sphere-packing density	Asymptotic packing density in high dimension: lower bounds (Rogers → Campos et al. → Klartag) and upper bounds (Cohn–Elkies LP).	Lower-bound ladder accelerated 2023–2025, all human. Aug 2026 Astra claims new upper bounds reaching the Cohn–Elkies threshold (Lean; peer review pending) — first claimed LLM step, upper-bound side only.
Cap-set bounds	Largest subset of \((\mathbb{Z}/3\mathbb{Z})^n\) with no three-term AP; FunSearch’s flagship.	LLM yes (FunSearch 2023; entry’s claim: largest asymptotic lower-bound improvement in ~20 years). Ladder too sparse to call a slope change.
Kissing number (esp. dim. 11)	Max equal non-overlapping spheres touching a central one; tabulated by dimension.	LLM/agent steps yes: AlphaEvolve 592→593 (2025), then collective agents to 604 (2026). Burst on one dimension, not a field-wide slope change.
Binary / spherical codes	Max code size at a prescribed minimum distance.	Aug 2026 Astra claims exponentially stronger upper bounds for all parameters (Lean; peer review pending). No assembled historical step-size baseline in this log yet.
Sums-and-differences / autoconvolution	Additive-combinatorics constants with multi-decade record ladders (AlphaEvolve’s clearest head-to-heads).	LLM steps yes; pooled AI median about +0.9% vs larger human medians; humans retook sums-and-differences within months; 2025 burst, not a new long-run slope.
Matrix-multiplication exponent \(\omega\)	Best exponent for asymptotic \(n\times n\) matrix multiplication.	No LLM step on the asymptotic \(\omega\) ladder (still slowing). Related small-matrix algorithms improved by AlphaTensor / AlphaEvolve — a different object.
Difference-basis / hexagon / min-overlap type bounds	Finite geometric/packing constants in the AlphaEvolve set.	LLM yes on a minority of targets (product claim: improved ~20% of 50-plus problems; matched ~75%). Many nudges are 4th–5th decimal; exception: difference-basis (record since 1972) moved only after Singer-code hints.
Busy Beaver \(\mathrm{BB}(5)\)	Exact fifth Busy Beaver value.	Settled 2024 by human+enumeration with machine checking (Coq), not LLM discovery. One-off exact value, not a tightening series.
Multicolor Ramsey \(R_k(3)\)	Growth of multicolor triangle Ramsey numbers.	Aug 2026 Astra claims \(R_k(3)=k^{\Theta(k)}\), resolving Erdős #183 (Lean; peer review pending).

Lists of open problems.

List	What it is	Status
Erdős problems	~1,217 community-catalogued problems; main high-volume corpus AI has been pointed at.	LLM flow yes: wiki freeze (2026-06-30) ~13 full AI-standalone resolutions; AlphaProof Nexus 9/353 ≈ 2.5%. Post-freeze Astra claims #146, #180, #183. Highest-profile single fall: unit-distance (May 2026). Still mostly long-tail; corpus history too short for a clean before/after slope.
OEIS conjectures	Mechanically stated conjectures from the OEIS.	LLM yes — AlphaProof Nexus 44/492 ≈ 9%; higher yield than Erdős, consistent with cheaper formalization.
AlphaEvolve problem set	DeepMind’s ~50–67 named open problems (67 directory entries, nearer ~50 distinct) used as an evolutionary-search testbed.	Product claim: improved ~20%, matched ~75% of 50-plus applied; step sizes usually small. Not a fixed historical list, so “slope” is ill-defined.
HorizonMath	100+ predominantly unsolved problems with cheap automated verification.	Models near 0%; two claimed GPT-5.4 Pro improvements pending expert review — a floor, not a discovery curve.
Equational Theories Project	Exhaustive implication graph among simplest magma laws (~22M edges), Lean-checked.	Completed 2024–2025 with human+automated (+ AI tooling) proofs. Decomposable formal sweep, not a prestige open-list fall rate.
Hilbert’s problems (1900)	23 century-defining challenges (plus vague/contested).	No AI-attributed fall. Ledger: 12 consensus-resolved rows (≈10 problem-numbers if Hilbert 18 is not split), 7 open, 9 contested/vague; last dated piece Hales 1998. See the fall timeline →.
Landau’s problems (1912)	Four classical prime problems (Goldbach, twin primes, Legendre, and primes of the form \(n^2+1\)).	All still open; no LLM contribution.
Scottish Book (1935–41)	193 numbered café problems from the Lwów school, plus a few decimal-numbered additions in Mauldin’s edition.	Omitted from the fall figure: Mauldin’s 2015 appendix mixes unsolved / no-commentary / unknown rows and is a decade stale; the 2026 survey updates some problems but not a complete fall ledger. No AI-attributed prestige fall known to this log.
Smale’s problems (1998)	18 “problems for the next century.”	Five resolved ledger rows: four human (Lorenz 2002, Poincaré 2003, smooth hyperbolicity 2007, average-case polynomial solving posted in 2016) and one AI-attributed negative resolution (Jacobian conjecture in dimension 3, Alpöge–Claude Fable 5, July 2026; independently formalized).
Millennium Prize Problems (2000)	Clay’s seven $1M problems.	1/7 resolved (Poincaré, Perelman 2003); none by AI. Useful as a public ceiling check; bad outcome variable because verification is expensive. Fall timeline →.
The Open Problems Project (2001–)	78 computational-geometry problems (Demaine–Mitchell–O’Rourke).	17 marked solved, settled, or closed in TOPP’s own status lines; 60 marked open and one partially closed. CS-adjacent measurement list rather than Clay-style prestige.

Math

The first two entries are the domain’s efficiency-series backbone: the exponent database that makes tightened bounds a dated outcome variable, and the series this log extracted from it. The prestige-list ledger is the control for the public open-problem stock. The entries after them are the AI results and demonstrations, then the benchmarks.

Analytic Number Theory Exponent Database, ANTEDB (2025)

Independent (academic database). Tao, Trudgian, and Yang’s ANTEDB systematically records known theorems, conjectures, and relationships for exponents appearing in analytic number theory: exponent pairs, exponential sum bounds, zero-density and moment bounds for the Riemann zeta function, large value estimates, additive energy bounds, and exponents governing prime distributions. It is the closest thing research mathematics has to a per-problem efficiency curve.

• Bounds are a continuous outcome variable; solved-or-not is a binary one. Each exponent is a number whose best known value is recorded with a date and a proof, so progress on it is a monotone dated series rather than a flag that flips once. This is what makes bounds, rather than problem counts, the natural analogue of a cost curve — this log’s argument for using the database, not a claim the database makes.
• That series has now been extracted and plotted. The database’s Python codebase can restrict the literature to results published up to a given year and then solve for the best bound derivable from that restriction, which turns the database into a dated efficiency curve. Six such series are extracted and plotted in a derived entry below [→ ANTEDB rates]; their halving times run from 82 to 1,204 years. The database’s own figures plot exponent-pair regions in parameter space rather than history, so the time series appears to be new here.
• The database is both human-readable and executable. Tao: “Information on these exponents is collected both in a LaTeX ‘blueprint’ that is available as a human-readable set of web pages, and as part of our Python codebase.” Formalization is aspirational rather than done: “In the future one could also imagine the data being collected in a Lean formalization, but at present the database only contains a placeholder Lean folder.”
• Automated search over the recorded relations already improved the state of the art. The launch paper reports “four new exponent pairs; several new zero density estimates; and new estimates on the additive energy of zeroes of the Riemann zeta function.” Tao describes how, and the parenthesis is the important part.¹
• That automation is optimization over a relation database, not an LLM agent. The improvement came from systematically combining bounds already in the literature. It is evidence about how much unpicked fruit sits in an uncollated literature, not about model capability. This distinction is this log’s.
• It is a living database, not a benchmark. It has no fixed problem set, no scoring rule, and invites contributions — “We are hoping that the ANTEDB will receive more contributions in the future, for instance expanding to other types of exponents, or to update the database as new results are obtained (or old ones added)” — so it cannot be used as a capability time series without imposing structure it does not have.
• The stated purpose is collation, and the hoped-for payoff is exactly the apple-picking mechanism. “By providing a centralized database, it aids in the verification and progression of results in the field, potentially leading to breakthroughs or simplifications in proofs.” A literature whose existing results have not been systematically combined is a tree with reachable fruit on it.
• It builds on an earlier static table. The precursor is Trudgian and Yang’s “Toward optimal exponent pairs.”
• Dates: precursor exponent-pair tables arXiv 2023-06-09 (v3 2024-07-15); Tao’s launch post 2025-01-28; blueprint PDF dated 2026-07-03; retrieved 2026-07-26.
• Bears on: Q1 growth rate, Q7 incidence, Q8 benchmarks.
• Links: repo · blueprint site · launch paper, arXiv 2501.16779 · Tao’s launch post · Trudgian and Yang precursor
• Status: verified against the repository README, the project page, and Tao’s launch post, retrieved 2026-07-26. The blueprint PDF carries a 2026-07-03 date, so the database is current. The launch paper has since been identified as arXiv 2501.16779, “New exponent pairs, zero density estimates, and zero additive energy estimates: a systematic approach” (Tao, Trudgian, and Yang, 2025-01-28), and is now cited; an earlier version of this entry recorded it as unidentified.

¹ Terence Tao, launch post, 2025-01-28: “…abstracting out various relations between these exponents that were implicit in many papers in this subject, we were then able to run computer-assisted searches to improve some of the state of the art on these exponents in a largely automated fashion (without introducing any substantial new inputs from analytic number theory).”

How fast analytic number theory’s exponents actually improve (2026)

This log’s synthesis. Not a source: a dated series extracted from the exponent database [→ ANTEDB] and put in the same units as the efficiency curves this project is built on. The math section of the argument asserts that tightened bounds are the right outcome variable for this domain because they give a monotone dated series rather than a binary solved-or-not; this is that series, actually built. As far as this log can establish, nobody had plotted the database’s contents against time before — the database’s own figures plot exponent-pair regions in parameter space, not history.

Best known value of thirty analytic-number-theory exponents against time, one panel per slice, extracted from ANTEDB.

Each panel is one slice of one exponent: the best value derivable from the literature available in that year, computed by the database’s own solver, with the year taken from the reference that established each input. Every panel runs from 0 to a little above its own earliest value, so the fraction of the panel’s height the line descends is the fraction of the bound that has been removed, and the panels can be compared by eye. Markers are the years the record changed. The dashed line on the \(A\) panels is the density hypothesis \(A\leq2\). Each panel states its first and last value, the ratio between them, the year of the last change, and the number of record changes. The ten slices per family are chosen to include the ones carrying standard names: \(\mu(1/2)\) is the Lindelöf exponent, and \(A(3/4)\) is the slice Ingham bounded in 1940 and Guth–Maynard improved in 2024. Values are as the database records them; the ratios and the choice of slices are this log’s.

Improvement over the whole record, plotted against the parameter, for all three families.

The same data reduced to one number per slice: the latest bound divided by the earliest, across the full grid of 20 points for \(\mu\), 19 for \(A\) and 19 for \(\beta\). Lower means more of the bound was removed. The dotted line at 1.0 is no improvement; the three \(\beta\) points sitting on it never changed once in the recorded window. The horizontal axis is \(\sigma\) for \(\mu\) and \(A\) and \(\alpha\) for \(\beta\), which are different parameters plotted on one axis for compactness. The grids and the ratios are this log’s arithmetic over the database’s values.

• How it was built. tools/antedb_extract.py runs against a checkout of the database, calls list_hypotheses(year=Y) to restrict the literature to results published up to each year, asks the database’s own solver for the best bound derivable from that restriction, and walks each derived bound’s dependency tree to attribute it. It writes two files, both vendored: antedb-bounds.csv for the six named slices and antedb-sweep.csv for the parameter grids. tools/sources_figures.py plots from those. Nothing here is quoted from a source, because no source states these series.
• A subtlety in what the dates mean. The value at year \(Y\) is what the database says was derivable in year \(Y\), not what somebody had written down. Those differ, and the difference is the database’s whole point [→ ANTEDB]: collating relations yields bounds nobody had stated. So this is a curve of available knowledge, not of published claims, and it is the more favorable of the two to plot.
• The Lindelöf exponent moved 13% in a century. \(\mu(1/2)\) falls from \(5/28 \approx 0.1786\) (van der Corput, 1920) to \(13/84 \approx 0.1548\) (Bourgain, 2017), through fifteen record changes. That is a factor of 0.867 over 97 years, an implied halving time of about 500 years. The conjectured value is 0, so a century of work by many of the strongest analytic number theorists closed about an eighth of the distance.
• The other five series run from 82 to 1,204 years per halving. \(A(9/10)\) is the fastest at about 82 years, falling 3.6 to 1.5 over 1921–1980 and then flat for 44 years. \(A(3/4)\) is 238 years, \(\mu(3/5)\) 541, \(\mu(7/8)\) 986, \(\mu(3/4)\) 1,204. Every one of these is a halving time measured in centuries.
• Set against the rates this project’s other entries measure, the gap is three orders of magnitude. Language-model pretraining efficiency halves about every 8 months and ImageNet about every 9 [→ Epoch on LMs, ImageNet]; the fastest physical cost curve in the OWID set, DNA sequencing, halves about every 8.6 months [→ efficiency rates]; ML hardware price-performance takes about 25 months [→ hardware price-performance]. The fastest exponent here is about 40 times slower than the slowest of those, and the slowest is about 1,800 times slower than pretraining efficiency. This comparison is the log’s, and the caveat below limits it.
• Progress is lumpy, and the flat stretches are long. \(A(3/4)\) has three records in 103 years: Carlson 1921, Ingham 1940, then nothing until Guth–Maynard 2024. Secondary accounts of that gap agree — after Ingham’s 1940 bound, “over the next eighty years, the only improvement to this bound has been small refinements to the o(1) error.” An 84-year plateau in a heavily-studied quantity is the same step-function shape the algorithms domain shows [→ Sherry and Thompson, SAT Museum, Bixby], now in mathematics.
• A discrepancy found by checking one value against its source paper. The database records Guth–Maynard as \(A(\sigma) \leq 15/(3+5\sigma)\), giving \(A(3/4)=20/9\approx2.222\), while the paper’s headline zero-density consequence is \(N(\sigma,T)\leq T^{30(1-\sigma)/13+o(1)}\), i.e. \(A=30/13\approx2.308\). The database’s recorded form is the stronger of the two. This log has not resolved which the paper’s own sharpest statement is, and the point is recorded because it illustrates what kind of artifact the database is: a live derived object whose entries can be sharper than the abstracts they come from, not a transcription.
• These six are slices, not the extent of what moves — a correction to an earlier version of this entry. The first version of this entry called six exponents “a small and non-random sample, chosen because the database happens to record them,” which understated the database badly. \(\mu\), \(A\) and \(\beta\) are functions of a parameter, so any point on them is a legitimate dated series, and a sweep across grids of 20, 19 and 19 points finds that nearly all of them move: every \(\mu(\sigma)\) point has between 8 and 18 record changes, every \(A(\sigma)\) point between 2 and 8, and 16 of 19 \(\beta(\alpha)\) points between 2 and 5. The six plotted above were chosen because they carry standard names and standard conjectures, not because they are the only ones with a history.
• The database is much larger than these three families. It holds 475 dated literature entries across ten hypothesis types, computed here from the entry set: zero-density estimates (155), upper bounds on \(\beta\) (141), exponent pairs (61), upper bounds on \(\mu\) (55), large value estimates (42), large value energy regions (13), plus four smaller types. Two of those types have no history at all in the recorded window — the zero-density energy estimates are three entries all from 1979, and the zeta large value estimate is a single 1978 entry — and the exponent pairs and large-value regions are points and polytopes rather than scalars, so turning them into a series needs a scalarization choice this log has not made. Derived quantities such as the prime-gap exponents, which the database computes from zero-density and energy estimates, are a further untouched family.
• Progress is strikingly non-uniform along each function, which is a Q7 observation with no AI in it. The second figure is the finding: the century’s improvement ratio varies from 1.00 to 0.20 depending only on where you look. \(A(\sigma)\) improves steadily more as \(\sigma\) approaches 1, ending at 0.20 of its 1921 value at \(\sigma=39/40\) against 0.97 at \(\sigma=21/40\). \(\mu(\sigma)\) is nearly flat at 0.87–0.95 across most of its range and then falls to 0.58 near \(\sigma=1\). \(\beta(\alpha)\) improves most at small \(\alpha\), reaching 0.25, and has a dead zone around \(\alpha \approx 0.30\) to \(0.45\) where three grid points never moved once. So within a single well-studied subfield, with no AI anywhere, the return to effort differs by a factor of five depending on which part of the parameter space is attacked. That is the incidence claim this project asks about, measured on human mathematics. The reading is the log’s.
• No AI has contributed to any of these bounds, and the negative is sourced rather than assumed. Three separate things establish it. The database’s own authors say AI integration has not happened: “one could also imagine integrating the ANTEDB with other tools, such as Lean or AI systems, but for now we have focused primarily on collecting the data and optimizing the relations between the exponents,” and “the database only contains a placeholder Lean folder” [→ ANTEDB]. The automation that did produce new bounds is linear-programming-style optimization over collated relations, not a model, and produced them “without introducing any substantial new inputs from analytic number theory.” And when an AI system was pointed at this area, it failed: Tao reports AlphaEvolve “struggled to take advantage of the number theoretic structure in the problem, even when given suitable expert hints” [→ AlphaEvolve mathematics]. Every record change in every panel above is attributed to a human paper, the latest being Guth–Maynard 2024 and Trudgian–Yang 2023.
• The stated reason is problem form, not difficulty, and it has a testable edge. Tao’s diagnosis distinguishes two possibilities and does not settle between them: “This could potentially be a prompting issue, or perhaps the landscape of number-theoretic optimization problems is less amenable to this sort of LLM-based evolutionary approach.” What did work needed algebraic structure a search could exploit — “AlphaEvolve does seem to do well when the constructions have some algebraic structure” — and these exponents are asymptotic inequalities rather than finite constructions with a computable score. That is a claim about the shape of the problem, so it predicts the AI-reachable part of mathematics is delimited by whether a candidate can be cheaply scored, not by how hard the mathematics is. Reading these panels alongside that failure is the log’s comparison, not Tao’s.
• A caution about crediting the automation that did work. The exponent-database improvements are a good case for the argument that collation finds unpicked fruit, but the credit belongs to a human-designed relation database and a solver. The attribution audit of the AI-discovery literature makes the parallel point about AlphaEvolve’s mathematical results — that the search space and the domain knowledge in the prompt, rather than the evolutionary machinery, are what determine performance [→ simple baselines]. In both cases what did the work was a human’s formalization of where to look.
• What this cannot support. The units are not comparable to a cost curve in the way the arithmetic above pretends. A cost curve’s denominator is money or compute; an exponent’s improvement has no denominator at all, because research effort per bound is unmeasured and certainly rose over the century — which is the fishing-out baseline that applies here as everywhere [→ ideas harder to find]. The grids are also uniform in the parameter, which is not a measure of mathematical interest: \(\sigma\) near 1 is easier territory as well as faster-moving, so the spread in the second figure mixes difficulty with attention. And none of these series has any AI in it: the latest entry is 2024 and the automated search that the database’s launch paper reports is optimization over collated relations rather than a model [→ ANTEDB]. So this fixes the pre-AI baseline for the math domain, which the domain previously lacked entirely, and measures no AI contribution whatever.
• One year fails inside the database’s own solver, and is dropped rather than patched. The \(\beta\) sweep cannot compute 1991: compute_best_beta_bounds raises a TypeError for that restriction of the literature. The extraction script reports the skip rather than silently omitting it, and the 1991 \(\beta\) column is therefore missing from the sweep. No other year fails, and \(\mu\) and \(A\) are unaffected.
• Dates: the underlying references run 1920 to 2024; extracted and plotted 2026-07-26 from the database as of that date.
• Bears on: Q1 growth rate, Q6 intertemporal, Q7 incidence, Q8 benchmarks.
• Links: extracted by tools/antedb_extract.py from the database recorded at ANTEDB; the CSVs are vendored at posts/data/apple-picking/antedb-bounds.csv and antedb-sweep.csv, and the figure is generated by tools/sources_figures.py.
• Status: derived — every value comes from the database entry named above via the extraction script, the halving times are this log’s arithmetic over those values, and nothing is quoted as though a source had said it. The two external checks are noted in the entry: the Guth–Maynard functional-form discrepancy, and the secondary account of the 1940–2024 plateau.

Sphere-packing lower bounds: a bound series accelerating, all of it human (1905–2025)

Independent (the standard record ladder for the asymptotic sphere-packing density, as recorded in the recent literature). A second century-long bound series for the math domain, chosen because it is the counter-case to a reading in which recent record-setting is where AI lives: this series’ two largest steps in eighty years land in 2023 and 2025, immediately before the highlighted 2026 period, and both are human theory.

• The ladder, with dates and finders. Minkowski–Hlawka (1905, with Hlawka’s general form 1943) improved the trivial saturation bound by a factor of about 2. Rogers (1947) gave the first asymptotically growing improvement, a factor of \(d\), with constant \(2/e\); Davenport and Rogers raised the constant to 1.68 the same year; Ball (1992) to 2; Vance (2011) to \(6/e\) for dimensions divisible by four, via Hurwitz lattices; Venkatesh (2013) got the first super-linear factor, \(d\log\log d\), but only along a sparse sequence of dimensions. Then Campos, Jenssen, Michelen and Sahasrabudhe (2023) obtained \((1-o(1))\,d\log d\,2^{-(d+1)}\) — the first asymptotically growing improvement on Rogers valid for all \(d\), after seventy-six years — and Klartag (2025) gained another whole power, \(c\,n^{2}2^{-n}\), by a new probabilistic method.
• The shape is the finding: recent acceleration with no AI in it. Four steps in the twentieth century, then four between 2011 and 2025, the last two of them the largest since 1947. The bend immediately precedes the highlighted 2026 period, but every step is a human proof and none of the papers involves a machine-learning system. It is the cleanest available warning against treating temporal proximity to the highlighted period as an AI effect. The reading is the log’s.
• Why this matters next to the exponent database. The two series are structurally the same object — a dated ladder of humans tightening an asymptotic constant — and they disagree about the recent trend: the analytic-number-theory exponents are flat or nearly so through the same window [→ ANTEDB rates], while this one accelerates. So “century-scale bound series do not move much” is not a general fact about mathematics; it is a fact about particular quantities, which is the non-uniformity the incidence question is about.
• A caution on comparing the steps. The functional form changes along the ladder — \(c\,d\,2^{-d}\) for the mid-century entries, then \(d\log d\), then \(n^{2}\) — so the constants are only comparable within the middle family, and no single scalar runs the length of the series. That is why this entry is a dated ladder of forms rather than a plotted numeric curve, and it is the same problem the AlphaEvolve baseline hit on asymptotic problems [→ record steps].
• A related 2024 milestone, recorded because it is machine-verified rather than AI-discovered. The fifth Busy Beaver value, 47,176,870, was proved and formally verified in Coq in 2024 by the distributed bbchallenge collaboration, enumerating 181,385,789 machines — the first Busy Beaver value ever formally verified, and the first exact value settled since 1983. It belongs in this document as a case where the machine did the checking for a human crowd, which is the validation-bottleneck pattern with the roles the theory predicts [→ validation bottleneck], not a case of AI discovery.
• Dates: records 1905, 1943, 1947 (twice), 1992, 2011, 2013, 2023, 2025; Busy Beaver milestones 1962, 1965, 1983, 1989 (champion), 2024 (proved). Assembled and read 2026-07-29. Vendored at posts/data/apple-picking/sphere-packing-lower-bound-records.csv.
• Bears on: Q1 growth rate, Q4 expertise, Q7 incidence.
• Links: Campos, Jenssen, Michelen and Sahasrabudhe · Vance · a recent survey recording the ladder
• Status: verified as to dates, finders and bound forms against the survey and the primary preprints named, retrieved 2026-07-29. The ladder is as that literature records it rather than as this log reconstructed it independently, and the mid-century constants were not checked against the 1947 and 1992 primaries. The Busy Beaver figures come from the collaboration’s own announcement.

Famous open-problem lists: when the prestige problems fall (1900–2026)

This log’s synthesis. Not a source: a dated ledger of prestige and corpus open-problem lists — Hilbert (1900), Landau (1912), Smale (1998), the Millennium Prize Problems (2000), and The Open Problems Project (2001–) — plus a stock panel for the Erdős catalogue. The Scottish Book is named among the prestige lists but omitted from the fall figure, because there is still no complete current fall ledger. Prestige lists are the ceiling check; Erdős and TOPP are measurement corpora AI systems can actually be pointed at. The figure is the overview’s second keystone above; the notes below are the scoring rules and caveats.

Each scored list uses one horizontal track per row, from the list’s start year to a dated solution landmark or to the present for still-open rows. Filled circles mark dated solution landmarks, hollow circles at the right edge mean currently open, and grey dotted rows are disputed or vague. TOPP uses the same track convention from 2001 for visual consistency, even though its 78 entries accumulated after the project began and this ledger does not encode each entry’s addition date. Its filled markers follow TOPP’s own solved, settled, or closed language rather than an independent consensus review; problem 12 is included because TOPP calls it “solved (in a certain sense),” although related worst-case questions remain open. The Scottish Book is named in the overview and table but not drawn: Mauldin’s 2015 appendix still mixes unsolved, no-commentary, and unknown-status rows into one category, that freeze is a decade old, and the 2026 arXiv survey updates selected problems without supplying a complete current fall ledger. Plotting the 2015 mixed category next to current-status lists would overstate what is known. The Erdős panel plots monthly status snapshots, plus 8 August 2026, rather than mathematical solution dates. Through July the points follow the project’s GitHub statistics history; the August endpoint uses the live website’s solved-status headline (565) together with that day’s GitHub Lean count, so the series changes source at its tip. The site itself warns that an open-to-solved status change can follow the underlying solution by weeks, months, or decades.

• What the figure shows at a glance. Prestige lists barely move through the highlighted 2026 period, but they no longer show zero AI-attributed falls. Millennium is 1/7 (Perelman 2003); Landau is 0/4; Hilbert has twelve consensus-resolved subproblem rows ending with Hales 1998; and Smale has five resolved rows, the latest the independently checked Alpöge–Claude Fable Jacobian counterexample in 2026. TOPP’s own status lines mark 17 of 78 entries solved, settled, or closed. Erdős is a large, changing catalogue with measurable recent status flow. The Scottish Book is omitted rather than plotted from a stale mixed-status freeze.
• How the ledgers were scored. Prestige resolved normally requires secondary-account consensus; Smale 16 is included because an explicit finite counterexample has been independently kernel-checked in both Lean and Isabelle, while formal peer review remains pending. TOPP resolved follows the project’s own Status/Conjectures line when it says solved, settled, or closed.
• What this cannot support. Comparing “12 Hilbert rows versus 1 Millennium problem versus 17 TOPP entries” as draws from one urn is a category error. Hilbert and Smale are split into subproblem rows, and TOPP uses its maintainers’ status language. The Erdős stock window cannot carry a clean before/after AI slope: it is short, the catalogue grew, and site-status dates need not be solution dates.
• Dates: lists posed 1900–2001; prestige resolutions as ledgered through the July 2026 Smale 16 counterexample; TOPP status lines through 2024 solves; Scottish Book deliberately not ledgered beyond naming the 2015/2026 status gap; Erdős snapshots Aug 2025–Aug 8 2026; assembled 2026-08-08. Vendored at famous-open-problem-lists.csv and erdos-database-history.csv.
• Bears on: Q1 growth rate, Q7 incidence.
• Links: Clay Millennium Prize Problems · Wikipedia: Hilbert’s problems · Wikipedia: Landau’s problems · Wikipedia: Smale’s problems · independent Lean verification of Smale 16 · independent Isabelle verification · Mauldin’s Scottish Book · 2026 Scottish Book update · TOPP · Erdős problems
• Status: derived — prestige and TOPP rows are transcribed into the vendored CSV from the named secondary accounts / TOPP status lines; Erdős stock is the existing monthly history; the Scottish Book is named but omitted from the figure because no complete current fall ledger is available. Disputed classifications are this log’s.

OpenAI: Erdős unit-distance disproof (2026)

Vendor result, independently verified. An internal general-purpose reasoning model disproved Erdős’s 1946 conjecture that the maximum number of unit-distance pairs among \(n\) planar points grows as \(n^{1+o(1)}\), producing a construction with growth \(n^{1+\delta}\) for fixed \(\delta>0\) (May 20 2026) (OpenAI 2026).

• Autonomy claim. OpenAI says the model was not specialized for mathematics, scaffolded to search proof strategies, or specifically targeted at this problem.
• Independent verification. Nine mathematicians produced a digested, human-verified account; Will Sawin separately made the exponent explicit at greater than 1.014.
• Why it is load-bearing. The problem was genuinely hard-fought for 80 years, and the construction combined ideas from algebraic number theory in a new discrete-geometric setting — external experts judged it a major result. It is the strongest counterexample to “shallow only” and to “neglected problems only.”
• Dates: conjecture posed 1946; OpenAI announcement 2026-05-20; the nine-mathematician remarks and Sawin’s explicit bound both reached arXiv the same day, 2026-05-20.
• Bears on: Q1 growth rate, Q2 autonomy, Q3 demand, Q7 incidence.
• Links: OpenAI · human-verified remarks, arXiv 2605.20695 · explicit bound, arXiv 2605.20579
• Status: verified against all three primary sources.

Erdős #728 (2026)

Independent writeup of an AI solve (Jan 2026). A combination of GPT-5.2 Pro and Aristotle produced a Lean proof described as the first Erdős problem “regarded as fully resolved autonomously by an AI system.”

• Autonomy caveat. The operator supplied the problem and interacted with the systems, so the autonomy claim depends on the writeup’s “non-significant human involvement” convention; it does not mean an AI independently chose the research target.
• Tao’s caveat. Tao stresses that #728’s original statement was ambiguous and that a problem sitting “open” for 50 years often means nobody seriously tried.
• Dates: Tao’s caveat posted 2026-01-07, five days before the writeup reached arXiv on 2026-01-12 (v5 2026-01-26) — so the caveat is not a response to the writeup.
• Bears on: Q2 autonomy, Q4 expertise.
• Links: arXiv 2601.07421 · Tao, Mathstodon
• Status: verified-abstract; Tao commentary verified.

Terence Tao commentary (2025–2026)

Independent (expert commentary). The most articulate skeptical account of AI’s mathematical contributions; several framings closely parallel the apple-picking model.

• Jumping machines. “These AI tools, they’re like jumping machines that can jump two meters in the air, higher than any human,” reaching “the tops of the lowest walls.” But “what they can’t do is jump a little bit, reach some handhold, stay there, pull other people up, and then try to jump from there. There isn’t this cumulative process.” [verified against transcript]
• No partial progress. “These tools either succeed or they fail. They’ve been really bad at creating partial progress or identifying intermediate stages that you should focus on first.” [verified against transcript]
• The arithmetic. “Fifty-odd problems have been solved with AI assistance, which is great, but there’s like six hundred to go.” Not a success rate: problem selection, effort, and failed attempts are unobserved.
• The long tail. Unsolved problems form a “long-tail distribution,” with automated harvesting concentrated “at the very end of the tail” — the easy, neglected problems clear first.
• Complementarity. (Blog, Mar 2026.) AI is “a complementary way to do mathematics… very different from a human style” — jagged, not uniformly superhuman.
• Dates: Mathstodon selection post 2025-11-22; long-tail post 2025-11-30; Atlantic piece February 2026; Dwarkesh interview 2026-03-20; blog post 2026-03-29.
• Bears on: Q1 growth rate, Q5 returns, Q7 incidence.
• Links: Dwarkesh transcript · Mathstodon (long tail) · Mathstodon (selection) · The Atlantic · terrytao.wordpress.com
• Status: key quotes verified against the Dwarkesh transcript.

AlphaProof Nexus: formal proof search on open problems (2026)

Vendor (Google DeepMind), with results posted to a community repository. The largest evaluation to date of AI on genuinely open mathematics, and the primary source for the autonomous-resolution rate this log previously recorded as dropped. Agents generate Lean proofs, so correctness is machine-checked rather than reviewed.

Solve rate against mean cost in dollars for four agent designs, on six Erdős problems.

A spend-response curve at a fixed problem: solve rate against mean cost in dollars, saturating on most panels well before the right edge. The variants differ in where they sit on the cost axis rather than in what they can eventually reach, which is scaffolding buying efficiency inside a fixed reachable set rather than extending it.

• 9 of 353 open Erdős problems, resolved autonomously, at a few hundred dollars each. This is a rate with a denominator — about 2.5% — which is rare in this literature and is the figure the Erdős wiki entry could not previously source [→ Erdős wiki]. Two of the nine had been open for 56 years.
• 44 of 492 OEIS conjectures proved. A second denominated rate, about 9%, on a different and more formalizable corpus. The gap between 2.5% and 9% is itself evidence on Q7: the more mechanically stated the problem set, the higher the yield.
• Named results outside combinatorics. Two of four open Hilbert-function problems in algebraic geometry, including Zanello’s roughly fifteen-year-old conjecture on log-concavity of pure O-sequences; a bipartite variant of the graph reconstruction conjecture and a 1996 Graffiti conjecture; and, in optimization, an exact \(O(1/t)\) convergence rate for anchored gradient descent-ascent found by discovering a new parameter schedule.
• Verification is the design principle, not an afterthought. The stated motivation is that human review of natural-language proofs is too expensive because of hallucination, so the system trades generality for compiler-checkable output. That is the validation-bottleneck thesis being engineered around rather than argued about [→ validation bottleneck].
• The ablation is the most interesting result for this project. A basic agent alternating generation with Lean verification solved all nine Erdős problems too; the full system’s advantage was cost, saving 2× to 5× on the hardest cases. Meanwhile simpler LLMs, and AlphaProof alone in tree-search mode, solved none. So the reachable set was set by having any verify-and-retry loop, and scaffolding sophistication bought efficiency within that set rather than extending it — which is what a reach ceiling looks like.
• It also found errors in the corpus. The agents identified several misformalizations in the literature, which is a contribution to the substrate rather than to the frontier, and a reason problem-count denominators are softer than they look.
• Dates: arXiv 2026-05-21 (v2 2026-06-08).
• Bears on: Q1 growth rate, Q2 autonomy, Q4 expertise, Q5 returns, Q7 incidence, Q8 benchmarks.
• Links: arXiv 2605.22763 · alphaXiv
• Status: verified-abstract — the headline rates, cost figures, named results, and ablation are checked against the abstract and the paper’s introduction as reproduced on arXiv and alphaXiv, retrieved 2026-07-26. The cost-response figure above was read from the v2 HTML on arXiv. The body has not been read in full, and the results have not been independently audited; treat the “autonomously” claim with the same care as the Erdős #728 case [→ Erdős 728].

FunSearch: cap sets and bin packing (2023)

Vendor (Google DeepMind), peer-reviewed in Nature. The first case of an LLM producing a new result on a recognized open mathematical problem, and the direct ancestor of AlphaEvolve. An LLM proposes programs; an automated evaluator scores them; the loop evolves.

• The largest improvement to the cap set lower bound in twenty years. FunSearch found constructions of larger cap sets than any previously known in some settings, including an improvement to the asymptotic lower bound.
• A practical algorithm, not only a construction. It also produced online bin-packing heuristics beating standard baselines on well-studied distributions, which is why it appears in the optimization literature as well as the math literature.
• It searches for programs, not answers. The stated advantage over AlphaTensor is generality and interpretability: a program describing how to build a solution transfers across problems and can be read by a mathematician, where a raw solution cannot.
• Why it matters for the timeline. It sets the start of the LLM-driven discovery era at December 2023, which means the cyber and algorithms results in this log sit roughly two years into the phenomenon rather than at its beginning. Any claimed acceleration should be measured from here.
• Scale caveat. The reported process was a few dozen iterations over a few days — small compared with the six- and seven-figure token budgets in the 2026 cyber entries. Cost per result is not comparable across those eras.
• Dates: published in Nature 2023-12-14, the same day as DeepMind’s announcement; a follow-up on combinatorial competitive programming appeared December 2024.
• Bears on: Q1 growth rate, Q2 autonomy, Q7 incidence.
• Links: Nature · DeepMind blog · MIT Technology Review
• Status: verified-abstract — checked against the Nature abstract, the DeepMind announcement, and contemporaneous reporting, retrieved 2026-07-26; vendor result, peer-reviewed.

AlphaProof and IMO 2024 silver (2024)

Vendor (Google DeepMind), peer-reviewed in Nature. The formal-reasoning system behind the 2024 olympiad result, and the year-earlier point that makes the 2025 gold interpretable as a trend rather than an event.

• Silver-medal standard at IMO 2024. AlphaProof solved three of the five non-geometry problems, including the competition’s hardest; combined with AlphaGeometry 2 the system reached a silver-medal-equivalent score. It was the first medal-level performance by an AI system.
• The compute caveat was substantial and is often dropped. The result was achieved with multi-day computation, against the 4.5 hours per paper human contestants get. The 2025 gold was obtained within the contest time limit [→ IMO 2025], so the two years differ in the constraint as well as the score.
• Test-time RL is the mechanism. For the hardest problems the system generates and learns from millions of related problem variants at inference time — problem-specific adaptation rather than a single forward pass, which is the same family of technique as the test-time training in the algorithms domain [→ TTT-Discover].
• Formal, therefore checkable. Proofs are produced in Lean, so the grading question that dogs natural-language claims does not arise. This is the same design choice as AlphaProof Nexus and the reason both can report clean denominators.
• Dates: IMO 2024 held July 2024, result announced July 2024; the Nature paper received 2025-06-03, accepted 2025-10-30, published 2025-11-12.
• Bears on: Q6 intertemporal, Q8 benchmarks.
• Unused: not yet cited in the argument. It converts the IMO entry from a single data point into a dated two-year series — silver under multi-day compute in 2024, gold within time limit in 2025 — which is the kind of comparison the Q6 row needs.
• Links: Nature
• Status: verified-abstract — checked against the Nature abstract and article metadata, retrieved 2026-07-26; vendor result, peer-reviewed.

Erdős-problems wiki: AI contributions (2026)

Independent (community-maintained). The “AI contributions to Erdős problems” wiki; data frozen 30 Jun 2026 (“no longer updated”).

• Counts. ~47 cases of AI-standalone contribution (non-significant human involvement): roughly 13 full resolutions, ~25 partial-progress, and ~9 incorrect. [verified against the wiki]
• The maintainers’ own disclaimers, verbatim: the list “is not a benchmark,” and “Absence of past progress may reflect obscurity rather than difficulty.” — a primary-source statement of the starting-point-dependence mechanism. [verified against the wiki]
• Recovered figure. An earlier draft cited a “9 of 353 (≈2.5%)” autonomous rate that the wiki does not carry, and this log dropped it pending a primary source. The source is DeepMind’s AlphaProof Nexus paper, where the nine resolutions were attempted against 353 open problems and then posted to this wiki [→ AlphaProof Nexus]. The figure is usable again, with the caveat that it is the vendor’s own denominator and the wiki is downstream of it rather than independent of it.
• Dates: data frozen 2026-06-30; retrieved 2026-07-26.
• Bears on: Q4 expertise, Q7 incidence, Q8 benchmarks.
• Links: teorth wiki
• Status: verified against the wiki snapshot; a reproducible recount from archived data is still owed.

GPT-5 literature retrieval (2025)

Mixed: a public mislabelling episode (October 2025) plus a later paper (November 2025). GPT-5 located published-but-forgotten solutions to about ten still-“open” Erdős problems — retrieval, not new math.

• A deleted tweet conflated retrieval with solving; Thomas Bloom clarified: “GPT-5 found references, which solved these problems, that I personally was unaware of.” The cautionary tale for classifying any claimed solve.
• The linked arXiv paper is a different object and should not be described as independent reporting of the episode. “Early science acceleration experiments with GPT-5” (2025-11-20) is a fourteen-author paper including OpenAI’s Sébastien Bubeck alongside academic mathematicians including Timothy Gowers. It is a set of case studies, part vendor and part independent, published a month after the episode. Treating it as the write-up of the retrieval incident conflates two things; if the argument cites it for anything beyond the retrieval point, the paper needs its own entry and its own status line.
• Dates: the mislabelling episode is October 2025; the arXiv paper is 2025-11-20 and is a separate object, see the caveat below.
• Bears on: Q4 expertise, Q8 benchmarks.
• Links: arXiv 2511.16072 · Scientific American
• Status: verified for the retrieval episode and Bloom’s clarification. The arXiv paper’s authorship and date were checked against its listing on 2026-07-26; its contents have not been read, which is why nothing is quoted from it.

IMO 2025 gold (2025)

Vendor results, one officially graded. July 2025: Google DeepMind’s Gemini Deep Think was officially graded at gold-medal standard, 5/6 problems for 35/42; OpenAI reported the same threshold but self-graded. Only 67/630 human contestants earned gold.

• Dates: IMO 2025 held July 2025; DeepMind’s officially graded result announced July 2025.
• Bears on: Q8 benchmarks.
• Links: DeepMind
• Status: verified (DeepMind); OpenAI figure self-graded.

Epoch AI: FrontierMath (2026)

Independent (benchmark). Research-level math benchmark; scores are model-and-evaluation-system results under a budget of up to one million tokens, not direct estimates of autonomous research success.

• Trajectory. From under 2% for launch-era models to much higher scores by 2026. On the corrected Tier 4 v2 leaderboard (checked July 23, 2026): GPT-5.2 Pro 46.0% ± 7.8%, GPT-5.4 Pro 58.5% ± 7.8%, highest listed 87.8% ± 5.2%.
• Revision caveat. Epoch released v2 on June 12, 2026 after addressing errors in 42% of problems: corrected 123 Tiers 1–3 problems and 12 Tier 4 problems, removed 5 and 7 respectively. v1 and v2 scores should not be joined into a clean capability time series.
• The benchmark’s funding and access arrangements were disclosed late, and that bears on the scores. OpenAI funded the benchmark’s creation and had visibility into its contents, which Epoch did not disclose until after the first headline results circulated. In TechCrunch’s account, Epoch “revealed on December 20 that OpenAI had supported the creation of FrontierMath,” and “In addition to backing FrontierMath, OpenAI had visibility into many of the problems and solutions in the benchmark — a fact that Epoch AI didn’t divulge prior to December 20.” Contributing mathematicians were not told: Carina Hong reported that “Six mathematicians who significantly contributed to the FrontierMath benchmark confirmed [to me] … that they are unaware that OpenAI will have exclusive access,” and “Most express they are not sure they would have contributed had they known.” Epoch’s co-founder Tamay Besiroglu: “we should have negotiated harder for the ability to be transparent to the benchmark contributors.”
• What that does and does not undermine. It is a transparency failure rather than a demonstrated contamination, and no entry here establishes that the disclosed access changed any reported score. But it means a FrontierMath score is not an arm’s-length measurement of the funder’s models, which is the standard the log’s Q8 rule asks for, and it is a second reason after the v2 revision not to build a capability series on this benchmark. This assessment is the log’s.
• Dates: funding disclosure 2024-12-20; TechCrunch report 2025-01-19; v2 released 2026-06-12; leaderboard checked 2026-07-23.
• Bears on: Q6 intertemporal, Q8 benchmarks.
• Links: Epoch Tier 4 v2 · skeptical: TechCrunch on the funding disclosure · contributor accounts
• Status: verified against the leaderboard and changelog; the funding-disclosure quotes verified against the TechCrunch report, retrieved 2026-07-26. Whether the disclosed access affected any score has not been established either way.

Kissing number: AlphaEvolve, a human in other dimensions, then agents (2025–2026)

Independent reporting. AlphaEvolve pushed the 11-dimensional kissing-number lower bound from 592 to 593 (May 2025). An earlier version of this entry said a mathematician then “improved the bound further” — that read too much into the press release, and the correction matters for what the sequence illustrates.

• What the human improvement actually was. The Aalto release covers Ganzhinov, whose peer-reviewed constructions beat AlphaEvolve’s bounds in dimensions 10 and 14 — and fell one short of AlphaEvolve’s 593 in dimension 11, where his 2022 preprint value of 592 was the record AlphaEvolve had improved on. So the human result is a best-in-other-dimensions story, not headroom above the machine on the same quantity.
• Dimension 11 has since moved again, to AI agents. Henry Cohn’s kissing-number table, as of 2026-06-22, lists the dimension-11 lower bound at 604, credited to a collective AI-agent platform (Bianchi, Kwon, Pappu and Zou, arXiv 2606.10402), with an intermediate 594 by the same route. The dated sequence 566 (1971) → 582 (1977) → 592 (2022) → 593 (2025, AlphaEvolve) → 604 (2026, agents) is assembled with sources in the record-steps synthesis [→ record steps].
• Dates: AlphaEvolve’s 593, May 2025; Ganzhinov’s dimensions-10-and-14 results reported 2025-10-23; the 604 listed on Cohn’s table as of 2026-06-22, its within-2026 date not pinned. Corrected 2026-07-28.
• Bears on: Q1 growth rate, Q3 demand.
• Links: Aalto University · Cohn’s kissing table · arXiv 2606.10402
• Unused: no longer cited in the argument after the 2026-07-29 resync; kept because its facts stand.
• Status: verified as to the correction against the Aalto release, Cohn’s table, and the primary preprints, checked 2026-07-28; the 594 intermediate step and the platform’s method are from secondary description only.

AlphaGeometry: olympiad geometry from synthetic data (2024)

Vendor (Google DeepMind), peer-reviewed in Nature. The neuro-symbolic system that produced the first medal-level olympiad result in a single subject, two years before the general-purpose math results in this section. It matters here because it is the clearest case of a narrow, verifier-rich domain falling first, and because its human comparator is stated.

• The score, with the same denominator as its comparators. “In a benchmarking test of 30 Olympiad geometry problems, AlphaGeometry solved 25 within the standard Olympiad time limit.” On the same set, “the previous state-of-the-art system solved 10 of these geometry problems” and “the average human gold medalist solved 25.9 problems.”
• The training substrate is enormous and entirely synthetic. The method generates its own curriculum: “resulting in a final training dataset of 100 million unique examples of varying difficulty, of which nine million featured added constructs.” There is no human proof corpus in the loop, which is what makes the result a statement about verifier-rich search rather than about imitation.
• What 25 against 25.9 does not establish. Matching an average gold medalist on olympiad geometry is matching a human on a problem class selected to be solvable in hours by a talented teenager with no literature access. The log’s math entries on open problems report rates two orders of magnitude lower [→ AlphaProof Nexus], and the gap between those two numbers is the distance between competition mathematics and research mathematics. This framing is the log’s.
• Dates: Nature paper and DeepMind announcement both 2024-01-17.
• Bears on: Q1 growth rate, Q2 autonomy, Q7 incidence, Q8 benchmarks.
• Links: DeepMind blog · Nature
• Status: verified against the DeepMind announcement, retrieved 2026-07-26, which restates the Nature paper’s figures; the Nature full text is behind an authentication redirect and was not read. Vendor result, peer-reviewed — so the figures are a vendor page’s restatement of a refereed paper, which is a weaker standing than reading the paper.

AlphaGeometry 2: past the average gold medalist (2025)

Vendor (Google DeepMind). The successor, with a Gemini-based language model and a wider domain language; part of the system behind the 2024 IMO silver [→ AlphaProof and IMO 2024]. It supplies a rare within-system dated efficiency gain at a fixed problem population.

• A dated gain on a fixed 25-year problem set. The system “significantly boosted the overall solving rate of AG to 84% on all geometry problems over the last 25 years, compared to 54% previously.” Because the problem population is fixed and historical, this is one of the few comparisons in the log that is not confounded by a changing task set — though the scaffold and the base model both changed between the two figures.
• The headline comparison. AlphaGeometry 2 “has now surpassed an average gold medalist in solving Olympiad geometry problems.”
• The authors’ own statement that autonomy is incomplete. They frame the work as “progress towards using AG2 as a part of a fully automated system that reliably solves geometry problems from natural language input” — so natural-language end-to-end autonomy is a goal here rather than a claimed result, which is worth holding against the more sweeping autonomy claims elsewhere in this section.
• Dates: arXiv 2025-02-05 (v3 2025-12-08).
• Bears on: Q1 growth rate, Q4 expertise, Q7 incidence, Q8 benchmarks.
• Links: arXiv 2502.03544
• Status: verified-abstract — the three quotes checked against the arXiv abstract, retrieved 2026-07-26; the body figures were not read. Vendor result, not peer-reviewed at the version read.

PutnamBench: a formal benchmark that started near the floor (2024)

Independent (academic, UT Austin and collaborators). A multi-language formalization of Putnam competition problems, used to measure neural theorem provers. It is in the log as a dated floor: a benchmark whose authors described it as barely tractable at release, against which later formal-proving claims should be read.

• Size and construction. “1692 hand-constructed formalizations of 640 theorems sourced from the William Lowell Putnam Mathematical Competition.”
• Coverage across proof assistants. “All the problems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations.”
• The authors’ own difficulty statement, which is the reason to record it. “These approaches can only solve a handful of the PutnamBench problems, establishing the benchmark as a difficult open challenge for research on neural theorem-proving.”
• Dates: arXiv 2024-07-15 (v2 2024-11-03).
• Bears on: Q1 growth rate, Q2 autonomy, Q7 incidence, Q8 benchmarks.
• Links: arXiv 2407.11214 · repository
• Status: verified-abstract — counts and quotes checked against the arXiv abstract, retrieved 2026-07-26. Current leaderboard standings were not checked, so the entry supports the 2024 floor and not any later figure.

The Equational Theories Project: 22 million implications, formally settled (2024–2025)

Independent (open collaboration of 33 authors including Terence Tao). A crowd-plus-machine project that determined every implication between the simplest equational laws on magmas, with automated provers and AI tools producing Lean-verified proofs. It is the log’s best case of the decomposable-subproblem structure that AI contribution appears to require, and it is a very different shape of contribution from a single headline solve.

• The scale, and that it was completed. The project settled “all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas.”
• How, and how it was checked. The result was reached “by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean” — so the verification question that dogs natural-language claims does not arise, at the cost of restricting the domain to what can be formalized.
• It produced mathematics, not only bookkeeping. “several new constructions of magmas satisfying specific laws were discovered.”
• Why the shape matters more than the count. Twenty-two million machine-checked implications is not twenty-two million discoveries; it is one exhaustive sweep of a space that was decomposable into millions of near-identical subproblems. That is the structural condition under which AI contribution scales in this log — cheap verification plus decomposition — and it is the opposite of the unit-distance disproof’s structure [→ unit-distance]. Reading a problem count from this entry would be a category error. This is the log’s assessment.
• Dates: project launched 2024-09-25 per Tao’s blog; arXiv 2025-12-08 (v2 2025-12-16).
• Bears on: Q2 autonomy, Q3 demand, Q4 expertise, Q7 incidence.
• Links: arXiv 2512.07087 · Tao’s project tour
• Status: verified-abstract — the scale figure, the method, and the new-constructions claim checked against the arXiv abstract, retrieved 2026-07-26. The contributor count comes from the author list; the division of labor between human and automated proofs was not established from the body, so the entry cannot support any statement about the machine share.

Aristotle: formally verified IMO 2025 proofs (2025)

Vendor (Harmonic AI), preprint. The system that, with GPT-5.2 Pro, produced the Erdős #728 proof [→ Erdős 728]. Its distinguishing design choice is that output is machine-checkable Lean rather than natural language, which is the same choice AlphaProof and AlphaProof Nexus make.

• The headline claim, from the abstract. The system achieves “gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems.”
• The architecture, which is where the claim’s content sits. It integrates “three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver.” A dedicated geometry solver alongside a general prover is the same division of labor as AlphaProof plus AlphaGeometry [→ AlphaGeometry 2], so “one system solved the olympiad” is a looser description than it sounds in both cases.
• The problem-level denominator is a vendor figure and is not verified here. Harmonic’s press materials state that the system produced formally verified proofs for five of the six IMO 2025 problems. That count does not appear in the arXiv abstract and this log has not confirmed it against the paper body; treat it as an unverified vendor figure, and do not pair it with the graded DeepMind result [→ IMO 2025] as though the two were measured the same way.
• Dates: press announcement 2025-07-28; arXiv 2025-10-01 (v2 2025-10-10).
• Bears on: Q2 autonomy, Q4 expertise, Q8 benchmarks.
• Links: arXiv 2510.01346 · press announcement
• Status: verified-abstract for the performance and architecture claims, checked against the arXiv abstract, retrieved 2026-07-26; vendor and unverified for the five-of-six count and for any benchmark figures, which were not confirmed against the paper text.

Ringer in Nature: mathematicians’ hands-on assessment of AlphaProof (2025)

Independent (Talia Ringer, News and Views, Nature). A researcher given temporary AlphaProof access reports her own use and canvasses colleagues. It is the most quote-rich independent account in the log of what a formal-proving system does in real research rather than on a benchmark, and the disagreement it records among named mathematicians is more informative than any single verdict.

• A concrete research use, with the timing that makes it striking. “AlphaProof proved one of the lemmas in under a minute, even though the student and their collaborator had been stuck on it for some time. It then disproved the other one, exposing a bug in a definition that the student had written, which they then fixed.” Note that the second half is the more interesting contribution: the system found an error in the human’s own formalization, which is the same substrate-correction role AlphaProof Nexus reports [→ AlphaProof Nexus].
• Ringer’s own bottom line, hedged in the sentence itself. “AlphaProof is the first AI tool I have used that I found concretely useful for writing proofs, a sentiment shared by some, but not all, of the mathematicians I have corresponded with.”
• The limitation that predicts where it fails, and it is a starting-point claim. “on problems that relied on concepts that, at the time of the IMO 2024 competition, had not been defined in mathlib, AlphaProof struggled.” Kevin Buzzard, whose formalization of Fermat’s Last Theorem was “full of what he described as ‘bespoke definitions’,” is quoted flatly: “‘In my experience,’ he wrote, ‘no AI system is anywhere near useful to me right now.’”
• And the contrasting positive, from Floris van Doorn. “‘If this becomes publicly available,’ he told me, ‘I can imagine a workflow where you just call AlphaProof on newly stated lemmas while you’re continuing your work on something else.’”
• The compute constraint is a distributional claim about who can do this. “The computational power needed to build AlphaProof is on a scale that academic groups do not have access to without industrial partners,” and building a problem-specific curriculum “is computationally expensive.” The curriculum itself: “The resulting formal statements — all 80 million of them — form the basis of the ‘curriculum’ that AlphaProof uses to teach itself to write proofs.”
• Why the disagreement is the finding. Two research mathematicians reach opposite verdicts on the same system, and the difference tracks whether their work rests on concepts already in the standard library. That is starting-point dependence stated by practitioners about their own work, and it is the sharpest Q7 evidence the Math section has. This reading is the log’s.
• Dates: published online 2025-11-12; print Nature vol. 651, 2026-03-19 issue. Cites the AlphaProof paper as Hubert et al., Nature 651, 607–613 (2026).
• Bears on: Q2 autonomy, Q3 demand, Q4 expertise, Q7 incidence, Q8 benchmarks.
• Links: Nature · open PDF
• Status: verified — full text read from the open Nature PDF and all quotes confirmed verbatim, retrieved 2026-07-26. It is commentary in a journal’s News and Views section rather than a peer-reviewed study, so the observations are testimony rather than measurement.

AlphaEvolve across 67 mathematical problems, including where it failed (2025)

Mixed: vendor system, academic authorship (Georgiev, Gómez-Serrano, Tao, and Wagner). The systematic test of AlphaEvolve on open mathematics, and the only source in this log that reports an AI system being pointed at analytic number theory and not working. Tao is a co-author here and a co-author of the exponent database [→ ANTEDB], so this is the same person assessing both, which is why it settles whether AI has contributed to the exponent bounds.

• The scope and the headline, from the abstract. “we considered a list of 67 problems spanning mathematical analysis, combinatorics, geometry, and number theory. The system rediscovered the best known solutions in most of the cases and discovered improved solutions in several.” Note the ordering: rediscovery is the modal outcome and improvement is the exception, which is the opposite emphasis from most coverage of the paper.
• It also generalizes, and it chains into proof systems. “In some instances, AlphaEvolve is also able to generalize results for a finite number of input values into a formula valid for all input values.” The pipeline goes further: results are combined “with Deep Think and AlphaProof in a broader framework where the additional proof-assistants and reasoning systems provide automated proof generation and further mathematical insights.” The finite field Kakeya case ran the whole chain — construction from AlphaEvolve, symbolic proof from Deep Think, formal verification in Lean by AlphaProof.
• Analytic number theory is the recorded failure, and this is the answer to whether AI has moved the exponent bounds. Tao’s account of the paper: “When testing the tool on analytic number theory problems, such as that of designing sieve weights for elementary approximations to the prime number theorem, it struggled to take advantage of the number theoretic structure in the problem, even when given suitable expert hints.”² The failure was not for want of expertise in the loop.
• What it does well is stated as a structural condition, not a difficulty level. Tao: “AlphaEvolve does seem to do well when the constructions have some algebraic structure.” The method needs the problem recast as a search over constructions with a computable objective, which is a statement about problem form rather than about how hard the mathematics is.
• The verifier is exploitable, and the authors say how they had to fix it. Scoring functions had to use “exact arithmetic (or interval arithmetic) instead of floating point arithmetic,” because the system otherwise games the score. That is the same shortcut-exploitation warning the optimization benchmarks report [→ PERFOPT, benchmark reliability], arriving in pure mathematics.
• On named conjectures it found the known extremal candidates and nothing beyond them. For Sidorenko’s, Sendov’s, and Crouzeix’s conjectures it “generally was able to locate the previously known candidates for optimizers… but did not locate any stronger counterexamples.” Reaching the known frontier and stopping there is what a reach ceiling looks like.
• The improvements are real and mostly very small, which the headline share conceals. Secondary reporting of the specific magnitudes: the Erdős minimum-overlap upper bound moved “from roughly 0.380927 to 0.380924,” described in the same sentence as a “fourth-decimal-place nudge”; an uncertainty inequality went “from approximately 0.3523 down to 0.3521”; a hexagon packing improved by “a reduction of about 0.3% in edge length.” Against those, the matrix-multiplication result is the outlier the coverage leads with, being “the first improvement, after 56 years, over Strassen’s algorithm.” The distribution of improvement sizes, not the count of improvements, is the quantity this log wants, and no source assembles it.
• Follow-up work has already passed it, using much smaller models. Two of the paper’s own problems were improved within weeks by an 8B open-weights model with test-time RL [→ ThetaEvolve], and an attribution audit finds random LLM sampling matches it on some problems [→ simple baselines]. So the 2025-11 result should not be read as a frontier-model capability level; the reachable set here appears to be set by the search space and the verifier rather than by the model.
• The authors maintain a live scoreboard, and it is the most useful single artefact here. The companion repository carries a per-problem page, a notebook for most problems, and a status.json classifying 43 of the 67: 19 where AlphaEvolve holds the record, 12 where it matched a known optimum, 8 where it came in below the record, and 4 recorded as former_record — problems where its result has since been surpassed. That last count is the vendor’s own admission that its results are being overtaken, which is stronger evidence than any outside commentary. The remaining 24 are unclassified, which is consistent with their not having a record to hold. Counts computed here from the repository as of 2026-07-26; the repository describes itself as “a live repository which we expect to expand and improve over time,” so these will move.
• The notebooks state the incumbent bound and usually cite it, which makes a historical baseline tractable. Of 68 notebooks, 32 state an explicit inequality and 40 carry a journal-style citation, generally for the bound AlphaEvolve was trying to beat — for instance the autoconvolution constant is given as “\(1.28 \leq C_1 \leq 1.5098\)” with the upper bound attributed to Matolcsi and Vinuesa (2010) and the lower to Cloninger and Steinerberger (2017). So the last step of each problem’s record sequence is largely supplied; the sequence before it is not, and assembling it is the missing work described in the known gaps below.
• The directory list double-counts, so 67 is not 67 distinct problems. At least twelve pairs are the same problem under two names, such as arithmetic_kakeya and arithmetic_kakeya_conjecture, or erdos_squares_in_a_square and squares_in_square. The count of distinct mathematical problems is nearer 50. Computed here from the repository’s experiments directory, not stated by the paper.
• Dates: arXiv 2025-11-03; Tao’s account of it posted 2025-11-05. The underlying AlphaEvolve system is the 2025 one recorded separately [→ AlphaEvolve].
• Bears on: Q1 growth rate, Q2 autonomy, Q4 expertise, Q7 incidence, Q8 benchmarks.
• Links: arXiv 2511.02864 · Tao’s account · companion repository · per-problem pages
• Status: verified as to the abstract and Tao’s account, unverified as to the body; vendor system with academic co-authors. The abstract was read verbatim from the arXiv listing and the author list and 2025-11-03 date confirmed there, retrieved 2026-07-26. The analytic-number-theory, algebraic-structure, exact-arithmetic and named-conjecture quotes are from Tao’s blog post rather than from the paper’s own text, which is why they are attributed to him; the paper’s full text was not read, so it has not been checked whether it words those points the same way. The improvement magnitudes are quoted from trade-press coverage rather than from the paper, and should be re-checked against it before the argument uses them.

² Terence Tao, “Mathematical exploration and discovery at scale,” 2025-11-05, continuing directly: “This could potentially be a prompting issue, or perhaps the landscape of number-theoretic optimization problems is less amenable to this sort of LLM-based evolutionary approach. In contrast, AlphaEvolve does seem to do well when the constructions have some algebraic structure, such as with the finite field Kakeya and Nikodym set problems.” The hedge is the author’s own and should travel with the claim.

ThetaEvolve: an 8B open model passes AlphaEvolve’s bounds (2025)

Independent (academic, seventeen authors, largely Microsoft-affiliated). The most direct follow-up to the AlphaEvolve mathematics paper, and the sharpest available evidence in the math domain that what set the reachable frontier was the search harness rather than the model.

• The framing, and the criticism of AlphaEvolve embedded in it. From the abstract: AlphaEvolve is “a closed-source system that evolves programs to improve bounds on open problems. However, it relies on ensembles of frontier LLMs to achieve new bounds and is a pure inference system that models cannot internalize the evolving strategies.” ThetaEvolve is offered as “an open-source framework that simplifies and extends AlphaEvolve to efficiently scale both in-context learning and Reinforcement Learning (RL) at test time, allowing models to continually learn from their experiences in improving open optimization problems.”
• A small open model beat a frontier-ensemble system on its own problems. The system reached new best-known bounds on two problems from the AlphaEvolve paper — circle packing and the first autocorrelation inequality — using DeepSeek-R1-0528-Qwen3-8B, an 8-billion-parameter open-weights model [→ AlphaEvolve mathematics]. On circle packing at N=26 the reported score is 2.6359857 against AlphaEvolve’s 2.63586276, an improvement in the fifth decimal place.
• This is the same pattern as the kernel records, in a different domain. A test-time-training harness on an older or smaller model overtaking a frontier system is exactly what TTT-Discover reports for GPU kernels [→ TTT-Discover]. Two independent instances in two domains is the strongest case the log has that scaffold, not model generation, is the moving part — which cuts directly against reading capability series as staircases at model releases. This comparison is the log’s.
• What it does not show. The improvements are in the fifth decimal place on problems already pushed by AlphaEvolve, so this is evidence about who can reach a frontier cheaply, not about extending it. Nothing here suggests the reachable set grew.
• Dates: arXiv 2025-11-28, three and a half weeks after the AlphaEvolve mathematics paper. Code released publicly.
• Bears on: Q2 autonomy, Q4 expertise, Q5 returns, Q6 intertemporal.
• Links: arXiv 2511.23473 · GitHub · alphaXiv overview
• Status: verified as to the abstract, unverified as to the results. The abstract, author list, and 2025-11-28 date were read from the arXiv listing, retrieved 2026-07-26. The circle-packing figures and the identification of the model and the two improved problems come from secondary summaries rather than the paper body, which has not been read, and the bound claims have not been independently checked.

HorizonMath: unsolved problems with cheap verification (2026)

Independent (academic, ten authors, largely Oxford-affiliated). A benchmark of unsolved problems chosen so that discovery is hard but checking is cheap. It is the closest existing work to the historical-baseline comparison this log wants, and it is worth an entry partly for what it does and partly for what it deliberately does not do.

• The design principle is the same one this project keeps finding behind every strong result. From the abstract: “Our benchmark targets a class of problems where discovery is hard, requiring meaningful mathematical insight, but verification is computationally efficient and simple.” That is the validation-bottleneck thesis used as a selection rule for building a benchmark [→ validation bottleneck].
• Scale, and the contamination argument for using unsolved problems. “a benchmark of over 100 predominantly unsolved problems spanning 8 domains in computational and applied mathematics, paired with an open-source evaluation framework for automated verification. Because these solutions are unknown, HorizonMath is immune to data contamination, and most state-of-the-art models score near 0%.” Near-zero scores make this the least saturated math benchmark in the log, against FrontierMath’s rise into the 40–90% range on hard tiers [→ FrontierMath].
• Two claimed improvements on published results, with the hedge attached. “we find two problems for which GPT 5.4 Pro proposes solutions that improve on the best-known published results, representing potential novel contributions (pending expert review).” The parenthesis is the authors’ own and is the part usually dropped.
• Its comparator is the current record, not the history of the record. The benchmark measures AI output against “best-known published results” and carries no dated record sequence, so it can say whether a model beat the incumbent but not whether beating it was unusual by historical standards. That is the gap this log’s inventory is built to close [→ AlphaEvolve inventory], and naming it is this log’s reading, not a criticism the paper makes of itself.
• Dates: arXiv 2026-03-16.
• Bears on: Q2 autonomy, Q7 incidence, Q8 benchmarks.
• Links: arXiv 2603.15617
• Status: verified as to the abstract, unverified as to the body — the abstract, author list, and date were read from the arXiv listing, retrieved 2026-07-26. The absence of any historical baseline was checked against the abstract and listing only; the body has not been read, so a dating component cannot be entirely ruled out.

Williams: what played to AI’s strengths in the unit-distance disproof (2026)

Independent (journalism, Understanding AI). The one piece of substantive outside contextualization this log has found of a headline AI mathematics result — as against reporting it or reproducing it. It matters because it proposes a mechanism for which problems AI takes, and the mechanism is not the one apple-picking proposes.

• The overall reading is continuity rather than discontinuity. The piece argues the Erdős unit-distance disproof [→ unit-distance] is evolutionary rather than revolutionary, and sets it against a short trajectory: “Three years ago, LLMs struggled to solve arithmetic problems. It was only last year that LLMs started acing high school mathematics competitions.”
• Two stated reasons the problem suited an AI, and the second is the interesting one. “OpenAI’s solution also had two properties that played to the strengths of AI models relative to humans. First, the eventual solution relied on applying sophisticated techniques from a quite different area of mathematics: algebraic number theory.” And: “Second, the reasoning process was such a grind — and seemingly unlikely to succeed — that most humans would not have thought it worth the trouble.”
• Why that second reason matters for this project. It describes a problem left unpicked not because it was out of reach but because the expected value did not justify the effort. That is a different selection mechanism from either obscurity or difficulty, and apple-picking does not contain it: a reach ceiling is about height, whereas this is about whose time is worth spending. It predicts AI’s comparative advantage lies in low-probability high-effort searches regardless of their depth, which would explain the hardened-code cyber finds as well [→ Mythos]. This reading is the log’s, not the author’s.
• Its conclusion on demand. “In the short to medium term, this points to a world where AI models complement humans but do not replace them.”
• Dates: published 2026-05-28, eight days after the disproof was announced.
• Bears on: Q3 demand, Q4 expertise, Q7 incidence.
• Links: Understanding AI
• Status: verified as to the quotations, which were read from the article, retrieved 2026-07-26; journalism rather than research, so the mechanism claims are the author’s interpretation and carry no measurement behind them.

References

OpenAI. 2026. “An OpenAI Model Has Disproved a Central Conjecture in Discrete Geometry.” May 20, 2026. https://openai.com/index/model-disproves-discrete-geometry-conjecture/.