Grant Sanderson (@3Blue1Brown) – AI disproved a famous math conjecture. Now what?

Benchmark Progression:

• Solving International Math Olympiad (IMO) gold-medal problems no longer signals AGI, as it is viewed as another benchmark that can be trained for.
• AI models achieved near-gold performance in 2024 but were hindered specifically by geometry problems requiring brute-force solvers and combinatorics problems requiring "playful" creativity.
• The "dirty secret" of the IMO is that the problems are increasingly solvable through training rather than requiring unique human creativity.
• The next significant frontier for AI is not solving existing problems but generating new conjectures and defining new mathematical objects.

Nature of Mathematical Discovery:

• Connection vs. Mountain Building: Solutions may arrive via "lightning bolts" (connecting disparate fields, e.g., Riemann hypothesis and random matrix theory) or "mountain building" (creating entirely new theories and abstractions, e.g., Group Theory).
• Verification Delays: Historically, the utility of new concepts (like Group Theory) can take 100+ years to validate, suggesting AI-generated breakthroughs may face similar delays in human recognition of value.
• Exposition Gap: There is a distinct difference between proving a theorem and explaining it; humans may shift roles from "doers" to "curators" and "explainers" of AI-generated insights.
• Compressed Understanding: The value of AI mathematics may lie in generating succinct, human-parsable explanations rather than long, incoherent proofs, though this is currently difficult to benchmark.

AI Advantages and Training Dynamics:

• Grindability vs. Verifiability: Progress in math and coding accelerates due to the ability to "grind" via parallel rollouts in deterministic, containerized environments, unlike computer use which lacks this scalability.
• Entropy Management: A key AI advantage is the ability to systematically increase entropy by spawning agents with different biases (e.g., trying to prove vs. disprove) to escape local context traps.
• Architecture vs. Data: Breakthroughs in connecting ideas are likely driven by training environments and data quality rather than specific model architectures or loss functions.
• Parallelization: Unlike human geniuses, AI can universally apply insights across all accessible problems without the constraints of individual lifespan or geography.

The Role of Formalization (Lean):

• Process vs. Outcome: While Lean (formal verification) is not strictly necessary for current progress (as natural language proofs are working), it enables endless, unsupervised expansion of knowledge bases (e.g., Mathlib).
• Human Trust: Formalization provides a "green checkmark" of correctness, reducing the labor cost for human mathematicians to verify AI-generated papers before engaging with them.
• Unsupervised Exploration: Formal systems allow AIs to explore vast spaces of logical consequences without human intervention, potentially discovering new axiom systems or theorems over long timeframes.

Future Economic and Social Impacts:

• Career Trajectories: The role of the mathematician is expected to shift toward curation, education, and mentoring, as the social and relational aspects of teaching are difficult to automate.
• Translation to Physics: While pure math breakthroughs (e.g., Navier-Stokes) may not immediately yield economic leaps, incremental improvements in PDEs and simulations will likely benefit engineering fields like aerospace.
• The "Curator" Economy: As AI generates an abundance of new mathematics, the primary economic value will lie in humans deciding which insights are useful and distilling them for practical application.
• Education Shift: Learning will move from reading text to curating human-authored resources and using LLMs to prune and navigate complex conceptual branches identified by those experts.

Specific Historical and Theoretical Examples:

• Galois and Group Theory: Lagrange, Abel, and Galois spent decades developing the intuition for solving quintic equations, but the utility of their insights was not recognized for a century until applications in physics and cryptography emerged.
• Riemann Hypothesis: Solutions may involve connecting analytic number theory with quantum physics or random matrix theory, a task AI may excel at due to its breadth of knowledge.
• ABC Conjecture: The attempt by Shinichi Mochizuki illustrates the risk of AI generating "alien" mathematics that humans cannot parse or verify for years.
• Unit Distance Problem: The recent disproof by AI demonstrates the ability to connect known constants and prove relationships, accelerating human understanding rather than just producing opaque results.