AlphaProof's Greatest Hits

Original Article ↗ Hacker News Discussion ↗

Advances in AI-powered theorem proving, such as DeepMind’s AlphaProof, are raising hopes that machines could soon tackle Olympiad-level problems and even long-standing conjectures, while also prompting skepticism about timelines, compute costs, and lack of technical transparency. Commenters debate whether formal proof systems coupled with LLMs could eventually enable “superhuman mathematicians,” help advance areas like P vs NP or the Riemann Hypothesis, and transform applied fields, or whether current results are closer to expensive brute force with narrow scope. Underlying the exchange are broader questions about the practical value of automated math, its energy and hardware demands, and how far formal reasoning can extend beyond pure mathematics into messy real‑world domains.

Scope of AlphaProof’s Achievement

  • AlphaProof solved difficult International Math Olympiad problems, sometimes needing ~3 days of compute per problem.
  • Some see this as clearly “superhuman” since most contestants failed these problems under tight time limits.
  • Others argue the time/compute cost is central to evaluating its importance; without hardware details, it’s hard to gauge efficiency.
  • Compared with brute-force proof search, AlphaProof likely represents a large shortcut, but how large is unclear.

Prospects for Major Open Problems (P vs NP, RH, FLT)

  • Opinions differ on whether AI will soon solve problems like P vs NP or the Riemann Hypothesis.
  • Some are optimistic about 5–10 year timelines for “superhuman mathematician” systems that invent new objects and tools.
  • Others think P vs NP may be independent of standard axioms or simply far beyond any foreseeable AI, so timelines are unknowable.
  • Current systems cannot even re-derive dense known proofs (e.g., Poincaré conjecture) in a usable way for humans.

Role of LLMs in Mathematical Discovery

  • Many expect near-term impact in assisting with lemmas, error checking, and formalization rather than headline breakthroughs.
  • Potential strengths: exploring large technical search spaces, finding surprising connections, suggesting combinatorial proofs for problems in other domains.
  • Skeptics doubt AI will soon create genuinely new, powerful mathematical concepts versus recombining existing ones.

Formal Proof Assistants and Verification

  • Lean and similar tools are central: they allow cheap, precise checking of proofs once formalized.
  • Formal verification can, in principle, detect errors in long or complex proofs and eliminate hallucinations for fully formal content.
  • However, formalization is laborious; many important real-world or historical statements cannot be straightforwardly encoded in such systems.

Limits of Automation and Decidability

  • Participants note that any proof (in a fixed formal system) is in principle reachable by enumerating all finite symbol sequences, but this is usually computationally infeasible.
  • Distinction is made between recursively enumerable (can eventually find a proof if it exists) and decidable (can always tell if one exists).
  • Some discuss possible independence of P vs NP or similar statements from standard axiom systems; AI cannot bypass such logical limits.

Compute, Data, and Access

  • There is concern that massive GPU/TPU requirements and lack of open details (paper, training cost, hardware) limit evaluation and replication.
  • Debate on whether large cloud providers or wealthy sponsors will fund math-focused systems, given unclear direct revenue.
  • Suggestions that open-source or community efforts are constrained by compute costs.

Broader Impact on Mathematics and Society

  • Some see automated theorem proving plus LLMs as a path to a “math endgame,” or at least a turning point for research practice and identity.
  • Others stress that many real-world problems lack the clean verification loop of pure math, so broader “intelligence” remains unsolved.
  • There is discussion of math vs. applied domains: even if AI excels at pure math, driving cars, understanding physics, or modeling society may remain harder.
  • Sociological concerns: big-tech might frame future breakthroughs as AI triumphs for PR and valuation rather than for mathematical community goals.

LLMs, Formal Languages, and Hallucinations

  • Several comments see a future in pipelines where natural language is converted to formal languages, then to provers/planners, then back to human-readable results.
  • This could sharply reduce hallucinations in domains where formalization is feasible (math, some engineering/science).
  • For fuzzier fields (history, sociology, psychology), participants are skeptical that formal methods can meaningfully eliminate hallucinations.

Benchmarks and Evaluation

  • Reference is made to new research-level math benchmarks suggesting current AI is still far from human research performance, though details and datasets are not always public.
  • Some criticize both AlphaProof-style announcements and benchmark claims as “hot air” without open data, but others trust the expertise of involved mathematicians.