proof beyond the machine's reach

Problem statement

No AI system can reliably verify, generate, or discover proofs for complex mathematical results. Large language models can pattern-match simple proofs and suggest proof strategies, but they hallucinate mathematical steps, fail at multi-step compositional reasoning, and cannot distinguish valid proofs from plausible-looking nonsense. Interactive theorem provers (Lean, Coq, Isabelle) provide formal verification but require months of expert human effort to formalize a single research-level proof. The gap between AI's pattern-matching capability and the rigorous logical reasoning required for mathematical proof remains vast.

Why this matters

The inability to automate proof verification is a bottleneck across mathematics, computer science, and engineering. Formal verification of safety-critical systems (aircraft control, autonomous vehicles, medical devices) requires proofs that currently demand expensive human experts. The Lean mathematical library (mathlib) represents >1 million lines of formalized mathematics — an impressive but tiny fraction of known mathematics. As AI is increasingly used in drug discovery ($2+ billion invested in AI pharma), materials design, and climate modeling, the lack of formal verification means these AI-generated results cannot be trusted with mathematical certainty. NSF's AIMing program was created specifically to develop AI tools for mathematical research.

What’s been tried and why it hasn’t worked

LLMs (GPT-4, Claude) can generate plausible proof sketches but fail at the multi-step logical reasoning required for non-trivial proofs — they don't maintain consistent logical state across reasoning chains. AlphaProof (DeepMind, 2024) solved some International Mathematical Olympiad problems by combining LLMs with formal verification in Lean, but only for competition-level problems with known solution types — not open research questions. Automated theorem provers (Vampire, E) handle first-order logic efficiently but mathematical proofs typically require higher-order reasoning and creative insight that these systems lack. Neural theorem provers (trained on Lean/Coq corpora) can suggest individual proof steps but cannot plan multi-step proof strategies, and their suggestion accuracy drops rapidly as proof depth increases.

What would unlock progress

A hybrid architecture that combines LLMs' pattern recognition and mathematical intuition with formal systems' logical rigor — using the LLM to propose proof strategies and the theorem prover to verify each step. Massive expansion of formalized mathematics databases (moving from 1 million to 100 million lines of formalized proofs) to provide better training data. New neural architectures designed specifically for compositional logical reasoning rather than adapted from language modeling.

Entry points for student teams

A team could benchmark existing LLMs on a curated set of undergraduate-to-graduate-level proof tasks, measuring accuracy, failure modes, and the types of mathematical reasoning that cause the most errors; ready-made statement sets exist and are openly licensed, so the semester goes into the analysis rather than into building the corpus — miniF2F (244 competition and undergraduate statements, translated across Lean, Isabelle, Metamath and HOL Light) and PutnamBench (1,724 formalizations from Putnam problems 1962–2025, of which 672 are Lean 4). A second door builds the same "difficulty map" from the formalization side, but at a scale a semester can actually close: take a textbook-level lemma chain rather than a theorem from a current research paper, formalize it in Lean 4 against mathlib (open source, Apache-2.0), and record at each step where AI assistance proposed a step that failed to typecheck, hallucinated a lemma name, or lost the proof state — the failure taxonomy is the deliverable, and it is the same taxonomy whether the target is a textbook lemma or a research result. Formalizing a current research paper is the version of this project that does not fit a semester: expert teams take a year or more, and the binding requirement is research-level command of the mathematics plus mathlib fluency, not tooling. Relevant skills: mathematics, formal methods, machine learning, programming in Lean/Coq.