Proof Crystallization

Joint with Guido Montúfar (UCLA Mathematics, Statistics & Data Science). Builds on AGRADE, our agentic AI grading system in production at UCLA.

Formal proof assistants such as Lean provide a rigorous standard for mathematical correctness, but their use requires substantial human expertise and effort. At the same time, large language models are increasingly capable of producing mathematical explanations, proof sketches, and candidate arguments. The central challenge is reliability: informal LLM-generated arguments may contain hidden logical gaps, hallucinated claims, circular reasoning, or unsupported reductions.

Proof Crystallization is an agentic preprocessing layer between informal mathematical reasoning and formal verification. Rather than asking a single model to produce a final proof, the system organises several LLM agents into specialised roles — construction, natural-language verification, adversarial critique, repair, and judgment — and forwards only the strongest candidates on to Lean or to a human reviewer.

The pipeline

• Argument constructor. Given a theorem, conjecture, or partial argument, proposes lemmas, proof steps, reductions, and candidate lines of reasoning.
• Natural-language verifier. Audits each step in natural language: does it follow from previous steps, are assumptions used correctly, are hidden regularity, measurability, algebraic, or finiteness conditions missing?
• Adversarial critic and repair loop. A critic searches for counterexamples, unsupported inferences, circular reasoning, and ambiguous claims; the constructor then repairs the proof candidate in response. The loop is designed to reduce hallucination and error propagation.
• Judge and triage. A judge agent aggregates constructor, verifier, and critic outputs and decides whether the candidate is rejected, returned for repair, sent to a human reviewer, or forwarded to Lean for formal verification.

Evaluation

We compare the multi-agent architecture against single-agent baselines on three benchmark classes:

• Lean-checkable examples, where formal verification provides a hard correctness signal;
• controlled perturbations of recent (post-cutoff) arXiv arguments, where valid arguments are modified to contain subtle errors that the system should detect;
• synthetic theorem families with certified ground truth — especially finite probabilistic models, graph-theoretic identities, and generating-function identities.

Why this team

The project grows directly out of practical experience: with Maciej Głuchowski we developed and deployed AGRADE, an agentic AI grading system now used in the UCLA Mathematics Department. Grading is itself a structured form of mathematical verification — a proposed solution is compared against a rubric, checked for correctness, and given justified feedback — and the construction–verification–critique loop is already running there in production.