Automation Without Understanding: AI proves math while US cuts human mathematician funding

What happened

Researcher Jun-Yong Park published an arXiv paper on July 12, 2026, arguing that as AI systems produce legitimate mathematics — including a 2026 AI disproof of an Erdos planar unit-distance conjecture — the US is simultaneously cutting federal support for human mathematicians, creating a critical verification gap.

Context and impact

The paper comes after GPT-5.6 Sol proved the Cycle Double Cover Conjecture in under an hour. Park contends that human mathematical capacity to audit AI reasoning is irreplaceable national infrastructure — unlike AI systems, it takes decades to rebuild once dismantled. He proposes requiring AI systems performing consequential reasoning to output in formal, machine-checkable form.

Details

• AI disproved Erdos planar unit-distance conjecture (2026)
• GPT-5.6 Sol proved Cycle Double Cover Conjecture in under 1 hour
• US cutting federal mathematician funding as AI math capabilities surge
• Proposed remedy: mandatory formal (Lean/Coq) output for consequential AI reasoning
• arXiv 2607.06377, July 12, 2026