Automation Without Understanding

Jun-Yong Park

REVIEW 2 major objections 4 minor 19 references

AI does math, US defunds mathematicians: a strategic error

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · glm-5.2

2026-07-08 07:46 UTC pith:IZSXLUCW

load-bearing objection Solid policy essay with a genuine synthesis; the formal verification proposal is the weakest link but the central argument holds. the 2 major comments →

arxiv 2607.06377 v1 pith:IZSXLUCW submitted 2026-07-07 math.HO

Automation Without Understanding

Jun-Yong Park This is my paper

classification math.HO MSC 00A99

keywords mathematical capacityAI reasoningformal verificationstrategic infrastructuremathematical trainingproof assistantsnational competitivenessErdős conjecture

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper argues that two concurrent developments — AI systems beginning to produce genuine research-level mathematics, and the United States degrading its pipeline for training human mathematicians — together constitute a strategic error. The central object is mathematical capacity: not a stockpile of theorems but a trained, institutional ability to verify, interpret, and challenge reasoning, built over generations and, the author claims, impossible to reconstitute on demand. The paper distinguishes sharply between a proof as a product (which machines can increasingly manufacture) and understanding as a capacity (which must be cultivated in human minds through years of supervised training inside functioning institutions). Using the May 2026 AI disproof of an Erdős conjecture as a case study, the author shows that even a machine-generated proof became knowledge only because a human community existed to absorb, simplify, and verify it. The paper then proposes four policy responses: preserve the full mathematical training pipeline, build an independent national AI-assurance capacity, stop requiring immediate applications from pure mathematics, and require that AI systems performing consequential reasoning expose their decision-critical claims in formal, machine-checkable form rather than as persuasive natural language.

Core claim

The paper's central claim is that mathematical capacity — the trained human ability to verify, interpret, and challenge reasoning — is a form of strategic infrastructure analogous to semiconductor capability or energy security, and that the United States is dismantling it at precisely the moment AI systems most require human oversight. The load-bearing distinction is between proof as a product and understanding as a capacity: machines can increasingly generate the former, but only sustained institutional training produces the latter. The author illustrates this with a concrete example from the formalization of the Erdős disproof in the Lean proof assistant, where the deepest class-field-theo

What carries the argument

mathematical capacity

Load-bearing premise

The paper's argument depends on the premise that mathematical capacity, once degraded, cannot be reconstituted on demand — that training pipelines and intellectual traditions take generations to rebuild. The author asserts this by analogy to officer corps and nuclear engineering cadres but provides no comparative historical evidence of failed or slow capacity reconstruction attempts.

What would settle it

A case in which a country successfully rebuilt a world-class mathematical workforce within a decade after severe institutional degradation would directly challenge the paper's central premise that mathematical capacity is non-reconstitutable on demand.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

If the argument is correct, any nation that allows its mathematical training pipeline to atrophy while relying on AI-produced reasoning will accumulate a growing stock of unverified or weakly verified conclusions in critical domains — military, financial, scientific, and infrastructural.
The proposal to require formal, machine-checkable proofs for consequential AI reasoning would, if adopted, create a regulatory category distinct from both opaque model outputs and natural-language explanations, shifting oversight from persuasion to auditable structure.
The Lean formalization episode — where automation could not bridge gaps in human-built mathematical libraries — suggests that formal verification infrastructure itself depends on the same human mathematical capacity the paper argues is at risk, creating a feedback loop: defunding training hollows out the very tools meant to check AI reasoning.
The framing of mathematical capacity as non-reconstitutable infrastructure, if accepted, would place mathematics funding decisions under the same strategic logic as semiconductor or defense industrial base policy, rather than under discretionary science-funding logic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The paper's argument implies a measurable proxy for national mathematical capacity: the depth and completeness of formal proof libraries (e.g., Lean's mathlib) for advanced topics, since these libraries are literally human mathematical knowledge translated line by line and their gaps directly constrain what automated verification can achieve.
If mathematical capacity is genuinely non-reconstitutable on short timescales, then the strategic calculus changes for any country weighing short-term AI investment against long-term mathematical training: the opportunity cost of defunding training is not linear but involves irreversible loss of institutional knowledge and mentorship chains that take generations to rebuild.
The paper does not address whether AI-assisted education could partially substitute for traditional mathematical apprenticeship. If AI tutors become capable of delivering personalized mathematical training at scale, the claim that capacity cannot be reconstituted on demand would need qualification — though the paper's surgical-training analogy suggests the author would view this as insufficient.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

Solid policy essay with a genuine synthesis; the formal verification proposal is the weakest link but the central argument holds.

read the letter

The main thing to know: this is a well-argued policy essay that synthesizes three threads — AI mathematical capability, the erosion of US mathematical training, and formal verification — into a coherent strategic argument. The synthesis itself is the contribution. The individual observations are not new (the 1984 David Report, mechanistic interpretability concerns, budget cuts), but the specific combination and the framing of mathematical capacity as infrastructure worth treating like semiconductor capability is genuinely useful and not something I've seen stated this directly elsewhere. The writing is strong. The distinction between proof-as-product and understanding-as-capacity is well-articulated. The Lean formalization evidence (refs 15, 16) is the essay's best concrete moment: showing that formalizing the Erdős disproof either produced placeholder structures that type-checked while proving nothing, or required taking deep class-field-theoretic results as unproven hypotheses. This does double duty — it supports the broader argument that formal verification *consumes* human mathematical capacity, and it grounds the abstract claims in something tangible. The historical grounding (David Report, China's five-year plans) is appropriate and not overdone. The soft spots are real but proportionate. The stress-test concern about the formal verification proposal is the most substantive one: the essay recommends mandating that AI systems expose consequential claims in machine-checkable form, but its own evidence shows formal verification struggling with pure mathematics. The essay acknowledges that valid proofs can rest on false premises, but it doesn't fully address the gap between mandating formal verification and the demonstrated state of the art. How would this work for military logistics or financial risk, which are messier than pure math? The essay would be stronger if it scoped the proposal to domains where formal verification is tractable, or acknowledged a phased approach. The reader's concern about the 'cannot be reconstituted on demand' premise is legitimate but minor — the analogy to officer corps and nuclear engineers is reasonable, and the essay doesn't need to prove this empirically to make its point. The 'dismantling' framing is slightly stronger than the evidence warrants, given that Congress rejected most cuts, but the essay is honest about this and pivots to institutional damage, which is fair. This is for policy-oriented readers, science administrators, and anyone thinking about AI governance. It deserves a serious referee — the argument is substantive enough to warrant engagement, and the formal verification proposal, even with its gaps, is worth refining rather than dismissing.

Referee Report

2 major / 4 minor

Summary. This essay argues that the simultaneous rise of AI-produced mathematics and the degradation of US mathematical training capacity constitutes a strategic error, and that mathematical capacity should be treated as strategic infrastructure. It draws on the May 2026 OpenAI disproof of an Erdős conjecture, NSF budget disruptions, doctoral program cuts at several universities, and Lean formalization difficulties to support its case, and proposes four policy measures including mandatory formal verification of consequential AI reasoning.

Significance. The essay is well-written and timely, addressing a genuine policy question at the intersection of AI capability and mathematical infrastructure. Its strengths include concrete, well-sourced examples: the Erdős disproof and its companion verification papers, specific NSF budget figures, named doctoral program reductions (GW, Harvard, Chicago), and the Lean formalization attempts (refs [15], [16]). The mechanistic interpretability example (Nanda et al., ref [14]) is well-chosen to illustrate the dependence of AI understanding on mathematical training. The comparison to China's 2019 and 2021 national plans for mathematics provides useful geopolitical context. The essay makes a falsifiable policy claim—that mathematical capacity cannot be rapidly reconstituted—and proposes specific, evaluable interventions.

major comments (2)

The essay's fourth and most concrete recommendation—that consequential AI reasoning 'should be required to expose their decision-critical claims in a formal, machine-checkable form'—is in tension with the essay's own evidence. References [15] and [16] demonstrate that formalizing even a pure mathematical proof in Lean either produced placeholder structures that 'type-checked while proving nothing' or required taking deep class-field-theoretic results 'as explicit unproven hypotheses, a hundred years of human work written directly into the theorem's signature as trust.' The essay acknowledges that 'a valid proof can still rest on false premises,' but this concedes a different point than the one its evidence raises: the formalization process itself can introduce invisible gaps that automated checking cannot detect. If formal verification cannot reliably handle pure mathematical proofs, the
The essay's load-bearing premise that 'a country cannot conjure a mathematical workforce on demand' (section 'A PROOF IS A PRODUCT') is asserted but not supported with comparative historical evidence. The 1984 David report example (ref [17]) actually suggests that capacity can be rebuilt with political will—Congress and the NSF responded with substantial funding increases—though the essay notes the commitment 'faded within a decade.' This example could be turned to support the essay's argument (the fading shows fragility), but as presented it partially undercuts the 'cannot be reconstituted' claim. The essay would benefit from engaging more directly with this tension: is the claim that capacity cannot be rebuilt, or that it can be rebuilt only slowly and at greater cost? The latter is more defensible and would strengthen the urgency argument.

minor comments (4)

The 'first-contact problem' section, while well-written, is more speculative than the rest of the essay and could be tightened. The superintelligence framing may distract from the more immediate and better-supported argument about consequential delegation.
The essay states the NSF appropriation 'keeps the NSF roughly flat, at $8.75 billion against roughly $9 billion the year before.' This is a reduction of approximately $250 million (about 2.8%), which is not strictly 'flat.' The phrasing is defensible but could be more precise.
The claim that 'more than $14 million in grants already promised to mathematics programs was clawed back' (citing ref [8], Scientific American) would benefit from specifying the time period more precisely (during which months?).
The essay's title and subtitle are effective, but the phrase 'dismantled, not by malice but by neglect' in the opening section could be read as inconsistent with the later description of NSF 'quietly cutting hundreds of its basic research programs' to fund a specific new initiative (refs [9], [10]), which sounds more deliberate than 'neglect.'

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for a careful and constructive report. Both major comments identify genuine tensions in the essay that warrant revision. On the first, we agree the formal verification recommendation needs sharper framing given the evidence from refs [15] and [16]; we will revise to acknowledge the limitations of formalization more directly while preserving the core policy claim. On the second, we agree the David report example partially undercuts the strong 'cannot be reconstituted' claim and will revise to the more defensible formulation the referee suggests.

read point-by-point responses

Referee: The essay's fourth recommendation—that consequential AI reasoning should be required to expose decision-critical claims in formal, machine-checkable form—is in tension with the essay's own evidence. Refs [15] and [16] show formalization either produced placeholder structures that type-checked while proving nothing, or required taking deep results as unproven hypotheses. The essay acknowledges that a valid proof can rest on false premises, but this concedes a different point: the formalization process itself can introduce invisible gaps that automated checking cannot detect. If formal verification cannot reliably handle pure mathematical proofs, the recommendation seems undercut.

Authors: The referee identifies a genuine tension that the essay does not adequately address. We concede that the current draft frames the fourth recommendation too strongly: it presents formal verification as a clean conversion of opaque persuasion into auditable structure, while the essay's own evidence from refs [15] and [16] demonstrates that formalization can fail in ways that are themselves opaque—placeholder structures that type-check without proving, or deep results imported as unproven axioms. The essay's caveat that 'a valid proof can still rest on false premises' does not address the referee's sharper point: the formalization process itself can introduce invisible gaps. We accept this criticism. In revision, we will reframe the fourth recommendation to acknowledge these limitations explicitly. The argument we can honestly defend is narrower than what the current draft implies: formal verification does not eliminate the need for human mathematical judgment but rather restructures where that judgment is applied—from assessing an entire natural-language argument to auditing the formalization's fidelity, its axiom choices, and its specification. The Lean examples actually support this narrower claim: both failures required human mathematicians to diagnose them, which is consistent with the essay's broader thesis that formal verification consumes mathematical capacity rather than replacing it. We will make this argument explicit and temper the recommendation accordingly. revision: yes
Referee: The essay's load-bearing premise that 'a country cannot conjure a mathematical workforce on demand' is asserted but not supported with comparative historical evidence. The 1984 David report example actually suggests capacity can be rebuilt with political will—Congress and the NSF responded with substantial funding increases—though the commitment faded within a decade. The essay would benefit from engaging more directly with this tension: is the claim that capacity cannot be rebuilt, or that it can be rebuilt only slowly and at greater cost? The latter is more defensible and would strengthen the urgency argument.

Authors: The referee is correct that the David report example, as currently presented, partially undercuts the strong claim that mathematical capacity 'cannot be conjured on demand.' Congress and the NSF did respond to the David report with substantial funding increases, which demonstrates that political will can produce a response. The essay notes that the commitment 'faded within a decade' but does not adequately engage with the fact that rebuilding did occur. We accept the referee's suggestion to reformulate. The more defensible claim—and the one we actually need for the argument—is that mathematical capacity can be rebuilt only slowly and at greater cost than it takes to lose it, and that the political will required is itself fragile. The David report actually illustrates this well: the response was real but insufficient to meet the report's own targets, and the commitment proved unsustainable. In revision, we will replace the categorical 'cannot be conjured' language with the more precise formulation the referee proposes, and we will draw the David report example more tightly into the argument: the episode shows not that rebuilding is impossible, but that it is slow, incomplete, and vulnerable to reversal—which strengthens rather than weakens the case for not allowing capacity to erode in the first place. revision: yes

Circularity Check

0 steps flagged

No circularity: argumentative essay grounded in external evidence, not a derivation chain

full rationale

This is an argumentative policy essay, not a mathematical derivation. Its central claims rest on publicly verifiable external evidence: budget figures from Science and Scientific American, the OpenAI Erdős disproof announcement, companion verification papers by independent mathematicians, Lean formalization attempts by unrelated teams, and historical policy documents (1984 David Report, Chinese five-year plans). No claim reduces to a fitted parameter, a self-citation, or a definitional identity. The author cites zero prior works by himself. The essay's most concrete proposal—mandatory formal verification of consequential AI reasoning—is supported by external evidence (refs [15], [16]) showing Lean formalization difficulties, which the essay honestly reports as limitations rather than concealing. The skeptic's concern that this evidence undercuts the proposal's feasibility is a correctness-risk argument about whether the proposal is well-calibrated, not a circularity argument. The essay contains no derivation chain, no fitted inputs repackaged as predictions, no self-citation, and no definitional reductions. Circularity score is 0.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

This is a policy essay with no mathematical derivation, no fitted parameters, and no invented entities. The axioms are domain assumptions about the nature of mathematical capacity, AI capability, and institutional resilience. There are no free parameters in the formal sense.

axioms (4)

domain assumption Mathematical capacity cannot be reconstituted on demand once the training pipeline is broken
Stated in 'A PROOF IS A PRODUCT' section: 'A country cannot conjure a mathematical workforce on demand.' This is the load-bearing premise for the urgency of the strategic-error claim.
domain assumption AI systems are producing genuine research-level mathematical discoveries, not merely calculation
Stated in 'THE MACHINES CAN DO MATHEMATICS' section, supported by the Erdős disproof example and IMO gold-medal performances. Treated as established fact.
domain assumption Formal verification of AI reasoning is feasible and useful for consequential decisions
Stated in 'WHAT WASHINGTON SHOULD DO' section, fourth proposal. The essay acknowledges limitations but assumes the approach is viable enough to mandate.
domain assumption The NSF budget cuts and program eliminations constitute a degradation of mathematical capacity rather than a temporary disruption
Underlies the 'QUIET DISMANTLING' section. The essay notes Congress rejected most proposed cuts and funding is roughly flat, but frames this as 'stabilization at a lower level of confidence.'

pith-pipeline@v1.1.0-glm · 10031 in / 2073 out tokens · 287090 ms · 2026-07-08T07:46:01.673254+00:00 · methodology

0 comments

read the original abstract

Two developments are unfolding at once: artificial intelligence systems have begun to produce genuine research-level mathematics, and the United States is weakening the pipeline that produces humans capable of understanding what such systems are doing. This essay argues that, taken together, these developments amount to a strategic error. Mathematical capacity, which is the trained ability to verify, interpret, and challenge mathematical reasoning, is not a byproduct of theorem production but a form of infrastructure, built over generations by institutions that cannot be reconstituted on demand. Drawing on the May 2026 AI disproof of a longstanding Erd\H{o}s conjecture on the planar unit distance problem and on recent disruptions to federal support for the mathematical sciences, the essay makes the case for treating mathematical capacity as a strategic asset on a par with semiconductor capability. It further proposes, among other measures, that AI systems performing consequential reasoning be required to expose their decision-critical claims in formal, machine-checkable form, converting part of AI reasoning from opaque persuasion into auditable structure.

discussion (0)

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages · 4 internal anchors

[1]

Erdős,On Sets of Distances of𝑛 Points, The American Mathematical Monthly,53, No

P. Erdős,On Sets of Distances of𝑛 Points, The American Mathematical Monthly,53, No. 5, (1946): 248–250

work page 1946
[2]

OpenAI,An OpenAI model has disproved a central conjecture in discrete geometry, May 20, 2026.openai.com/index/model-disproves-discrete-geometry-conjecture

work page 2026
[3]

N.Alon,T.F.Bloom,W.T.Gowers,D.Litt,W.Sawin,A.Shankar,J.Tsimerman,V.Wang,and M.MatchettWood,Remarksonthedisproofoftheunitdistanceconjecture,arXiv:2605.20695, May 2026. 8

work page internal anchor Pith review Pith/arXiv arXiv 2026
[4]

An explicit lower bound for the unit distance problem

W. Sawin,An explicit lower bound for the unit distance problem, arXiv:2605.20579, May 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026
[5]

deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level

Google DeepMind, AlphaProof and AlphaGeometry teams,AI achieves silver-medal standard solving International Mathematical Olympiad problems, July 2024. deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level

work page 2024
[6]

GoogleDeepMind,ThangLuongandEdwardLockhart,AdvancedversionofGeminiwithDeep Think officially achieves gold-medal standard at the International Mathematical Olympiad, July 2025

work page 2025
[7]

OpenAI, announcement of gold-medal performance on the 2025 International Mathematical Olympiad, July 2025

work page 2025
[8]

E. R. Hasson,Can U.S. math research survive NSF funding cuts?, Scientific American, July 2025

work page 2025
[9]

Mervis,Exclusive: NSF slashes research programs to support new tech initiative, insiders say, Science, June 2026

J. Mervis,Exclusive: NSF slashes research programs to support new tech initiative, insiders say, Science, June 2026

work page 2026
[10]

National Science Foundation, announcement of the NSF X-Labs program, May 14, 2026

work page 2026
[11]

Alonso,George Washington U pauses admissions to 5 Ph.D

J. Alonso,George Washington U pauses admissions to 5 Ph.D. programs, Inside Higher Ed, January 26, 2026

work page 2026
[12]

devastating

G. Jakubowski,CCAS to shrink, halt doctoral program admissions in “devastating” 7 percent package cut, The GW Hatchet, January 26, 2026

work page 2026
[13]

Zahneis,Has the graduate-school collapse begun?, The Chronicle of Higher Education, December 3, 2025

M. Zahneis,Has the graduate-school collapse begun?, The Chronicle of Higher Education, December 3, 2025

work page 2025
[14]

Progress measures for grokking via mechanistic interpretability

N. Nanda, L. Chan, T. Lieberum, J. Smith, and J. Steinhardt,Progress measures for grokking via mechanistic interpretability, arXiv:2301.05217, 2023

work page internal anchor Pith review Pith/arXiv arXiv 2023
[15]

LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

Y. Zhang, Y. Sun, T. Suzuki, J. D. Lee, and F. Liu,LeanMarathon: Toward reliable AI co-mathematicians through long-horizon Lean autoformalization, arXiv:2606.05400, June 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026
[16]

Repository:github.com/logical-intelligence/erdos-unit-distance

A.Fetisov,AlephProverFormalizedPlanarUnitProblemDisprove, LogicalIntelligence, May 28, 2026. Repository:github.com/logical-intelligence/erdos-unit-distance. 9

work page 2026
[17]

National Research Council, Ad Hoc Committee on Resources for the Mathematical Sciences (E.E.David,Jr.,chair),RenewingU.S.Mathematics: CriticalResourcefortheFuture,National Academy Press, Washington, D.C., 1984

work page 1984
[18]

61, July 2019

Ministry of Science and Technology, Ministry of Education, Chinese Academy of Sciences, andNationalNaturalScienceFoundationofChina,WorkPlanforStrengtheningMathematical Science Research, Guo Ke Ban Ji [2019] No. 61, July 2019

work page 2019
[19]

Jun–Yong Park —june.park@sydney.edu.au School of Mathematics and Statistics, University of Sydney, Australia 10

Outlineofthe14thFive-YearPlan(2021–2025)forNationalEconomicandSocialDevelopment andLong-RangeObjectivesThroughtheYear2035,adoptedbytheNationalPeople’sCongress, March 2021. Jun–Yong Park —june.park@sydney.edu.au School of Mathematics and Statistics, University of Sydney, Australia 10

work page 2021

[1] [1]

Erdős,On Sets of Distances of𝑛 Points, The American Mathematical Monthly,53, No

P. Erdős,On Sets of Distances of𝑛 Points, The American Mathematical Monthly,53, No. 5, (1946): 248–250

work page 1946

[2] [2]

OpenAI,An OpenAI model has disproved a central conjecture in discrete geometry, May 20, 2026.openai.com/index/model-disproves-discrete-geometry-conjecture

work page 2026

[3] [3]

N.Alon,T.F.Bloom,W.T.Gowers,D.Litt,W.Sawin,A.Shankar,J.Tsimerman,V.Wang,and M.MatchettWood,Remarksonthedisproofoftheunitdistanceconjecture,arXiv:2605.20695, May 2026. 8

work page internal anchor Pith review Pith/arXiv arXiv 2026

[4] [4]

An explicit lower bound for the unit distance problem

W. Sawin,An explicit lower bound for the unit distance problem, arXiv:2605.20579, May 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026

[5] [5]

deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level

Google DeepMind, AlphaProof and AlphaGeometry teams,AI achieves silver-medal standard solving International Mathematical Olympiad problems, July 2024. deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level

work page 2024

[6] [6]

GoogleDeepMind,ThangLuongandEdwardLockhart,AdvancedversionofGeminiwithDeep Think officially achieves gold-medal standard at the International Mathematical Olympiad, July 2025

work page 2025

[7] [7]

OpenAI, announcement of gold-medal performance on the 2025 International Mathematical Olympiad, July 2025

work page 2025

[8] [8]

E. R. Hasson,Can U.S. math research survive NSF funding cuts?, Scientific American, July 2025

work page 2025

[9] [9]

Mervis,Exclusive: NSF slashes research programs to support new tech initiative, insiders say, Science, June 2026

J. Mervis,Exclusive: NSF slashes research programs to support new tech initiative, insiders say, Science, June 2026

work page 2026

[10] [10]

National Science Foundation, announcement of the NSF X-Labs program, May 14, 2026

work page 2026

[11] [11]

Alonso,George Washington U pauses admissions to 5 Ph.D

J. Alonso,George Washington U pauses admissions to 5 Ph.D. programs, Inside Higher Ed, January 26, 2026

work page 2026

[12] [12]

devastating

G. Jakubowski,CCAS to shrink, halt doctoral program admissions in “devastating” 7 percent package cut, The GW Hatchet, January 26, 2026

work page 2026

[13] [13]

Zahneis,Has the graduate-school collapse begun?, The Chronicle of Higher Education, December 3, 2025

M. Zahneis,Has the graduate-school collapse begun?, The Chronicle of Higher Education, December 3, 2025

work page 2025

[14] [14]

Progress measures for grokking via mechanistic interpretability

N. Nanda, L. Chan, T. Lieberum, J. Smith, and J. Steinhardt,Progress measures for grokking via mechanistic interpretability, arXiv:2301.05217, 2023

work page internal anchor Pith review Pith/arXiv arXiv 2023

[15] [15]

LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

Y. Zhang, Y. Sun, T. Suzuki, J. D. Lee, and F. Liu,LeanMarathon: Toward reliable AI co-mathematicians through long-horizon Lean autoformalization, arXiv:2606.05400, June 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026

[16] [16]

Repository:github.com/logical-intelligence/erdos-unit-distance

A.Fetisov,AlephProverFormalizedPlanarUnitProblemDisprove, LogicalIntelligence, May 28, 2026. Repository:github.com/logical-intelligence/erdos-unit-distance. 9

work page 2026

[17] [17]

National Research Council, Ad Hoc Committee on Resources for the Mathematical Sciences (E.E.David,Jr.,chair),RenewingU.S.Mathematics: CriticalResourcefortheFuture,National Academy Press, Washington, D.C., 1984

work page 1984

[18] [18]

61, July 2019

Ministry of Science and Technology, Ministry of Education, Chinese Academy of Sciences, andNationalNaturalScienceFoundationofChina,WorkPlanforStrengtheningMathematical Science Research, Guo Ke Ban Ji [2019] No. 61, July 2019

work page 2019

[19] [19]

Jun–Yong Park —june.park@sydney.edu.au School of Mathematics and Statistics, University of Sydney, Australia 10

Outlineofthe14thFive-YearPlan(2021–2025)forNationalEconomicandSocialDevelopment andLong-RangeObjectivesThroughtheYear2035,adoptedbytheNationalPeople’sCongress, March 2021. Jun–Yong Park —june.park@sydney.edu.au School of Mathematics and Statistics, University of Sydney, Australia 10

work page 2021