I vibed a proof of Conway's conjecture

Original Article ↗ Hacker News Discussion ↗

An amateur mathematician describes using large language models and the Lean proof assistant to “vibe” their way to a formal proof of Conway’s surreal numbers refinement conjecture, sparking debate over authorship, credit, and what it means to “understand” a result. Commenters delve into how surreal numbers are constructed, the role of visualization and intuition versus formalism, and whether AI-driven proofs without human comprehension advance or damage mathematical culture. The thread broadens into questions about AI’s limits in mathematics, the impact on careers and incentives in pure math, and whether future work should prioritize conceptual insight over brute-force problem solving by machines.

Surreal numbers and “nothing vs zero”

  • Many readers got stuck at the “between nothing and zero / between zero and nothing” step.
  • Several commenters re-explained surreals in set-theoretic terms: numbers as {L | R} with L,R sets of earlier surreals; ∅|∅ as 0, ∅|{0} as –1, {0}|∅ as 1, etc.
  • Clarifications stressed: “nothing” = empty set, not 0; gaps include “to the left of all” and “to the right of all”.
  • Diagrams and external intros (e.g., Hackenbush, other blogs) were recommended as clearer than raw definitions.
  • Questions about how irrationals and infinities appear were answered via infinite stages: Dedekind-cut–like constructions and infinite left/right sets yield reals, infinite ordinals, and infinitesimals.

AI tutoring and pedagogy

  • Some wish for adaptive, RL-style interactive tutors that model individual understanding and fill gaps.
  • Suggestions included prompting for analogies in domains one already knows and using existing “teaching skills” setups.

AI’s role in mathematics: power and limits

  • Debate over whether LLM-driven proofs are “intelligent” or just large-scale brute force.
  • Some argue efficient exploration of huge search spaces is itself a mark of intelligence; others compare it to fast but “dumb” 1980s CPUs.
  • Theoretical discussion references Busy Beaver, the halting problem, and Gödel: any fixed computational system (including LLMs) cannot decide all true mathematical statements.
  • Counterpoint: most undecidable/independent propositions are “ugly and irrelevant”; practical math may rarely hit these limits.

Verification, Lean, and trust

  • The Lean formalization is seen as central: if the small bridge file and the kernel are correct, the proof stands.
  • Some worry about Lean/kernel bugs and recent “LLM hacks”; others note cross-checking with independent kernels and limited trusted code.
  • There is interest in extracting reusable surreal-number infrastructure into mainstream Lean libraries.

Credit, authorship, and mathematical culture

  • Strong disagreement over calling this “my proof”:
    • One side: using an LLM is like using a powerful tool (a drill); the human chose the problem, orchestrated runs, curated outputs, and bears responsibility for errors.
    • Opposing side: the human provided almost no mathematical insight, so taking credit is misleading and culturally corrosive.
  • Broader worries:
    • “Strip-mining” math for results without understanding may demotivate human researchers and damage career structures.
    • Fear that mid-level mathematicians will lose already-scarce opportunities, while only a few senior figures or famous problems benefit.
    • Others counter that systematizing, simplifying, and turning obscure AI proofs into short, elegant human ones is itself substantial work.

Reactions to the project and its style

  • Many readers enjoyed the post as “epistemic performance art” and an unusually accessible, self-aware narrative of working with fallible models.
  • Some appreciated seeing an “amateur” stumble through high-level math, finding it more relatable than expert lectures.
  • Skeptics found the project “immoral,” uncreative, or unhelpful to understanding, despite acknowledging that the underlying result (if correct) is mathematically nontrivial.
  • A key human expert on the underlying area reports that the AI-generated method appears sound and that the core ideas can be distilled into a very short, elegant proof, reinforcing hope for constructive AI–human collaboration.