Skip to content

MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research

🕒 Published (v1): 2026-07-16 05:22 UTC · Source: Arxiv · link

Why this paper was selected

Human-AI symbiotic paradigm for math; novel human-in-loop agent scaffold for scientific discovery

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

MathCoPilot is a human-in-the-loop system that restructures formal theorem proving as a collaborative workflow: the mathematician steers proof strategy while AI agents handle Lean 4 formalization and verification. It introduces a "living proof blueprint" — an interactive flowchart of proof sub-steps — through which humans direct agents at any granularity. Experiments on FormalMATH and real PDE theorems reveal that NL-first proving roughly doubles strict Lean verification rates over formalization-first, but domain-specific research-level theorems remain substantially unsolved.

Problem

Existing LLM-based theorem provers operate as autonomous Q&A systems that output monolithic end-to-end proofs, leaving mathematicians unable to inject high-level direction mid-proof, inspect intermediate logical steps, or adapt strategies based on domain intuition. They also lack support for the broader research workflow: paper ingestion, long-term lemma accumulation, and interactive proof refinement. Comparative evaluation of models and strategies is obscured by single-number pass rates that hide sensitivity to proving skill and autoformalization choices.

Method

MathCoPilot unifies three components under a Lean 4 verification backend and a personal verified knowledge base:

  1. Interactive proof co-construction via blueprint: Five specialized agents — Brainstorm, Blueprint, Prover, Formalizer, Aggregation — operate on a shared, editable flowchart of proof nodes. The mathematician clicks into nodes to inspect, edit, or trigger recursive sub-decomposition; the Formalizer emits a Lean skeleton with sorry placeholders that gets filled as nodes are discharged. Recursion to arbitrary depth converts hard nodes into provable leaves.

  2. Adaptive proving skill orchestration: A skill orchestrator dynamically selects among skills (NL-first: informal sketch → incremental Lean translation; formalization-first: work directly from the formal statement; knowledge-grounded: retrieve analogous lemmas before proof construction). Lean error feedback (type mismatches, missing hypotheses, unsolved goals) drives skill switching and retry logic.

  3. Automated knowledge base construction: Given a user-specified topic, the system retrieves papers from Semantic Scholar, arXiv, and Mathlib, extracts formal definitions and theorem statements via an extraction agent, translates them into Lean 4 in dependency order, verifies compilation, and indexes entries by topic tags and dependency graphs. Each entry stores both verified Lean code and the natural-language reasoning chain that produced it.

Key Contributions

  • A human-in-the-loop proof paradigm with a node-local, pointing-based blueprint interface enabling mathematicians to control proof direction without back-and-forth dialogue
  • An adaptive skill orchestrator that dynamically switches between NL-first, formalization-first, and knowledge-grounded proving strategies based on Lean feedback
  • An automated pipeline for ingesting external papers into a personal verified Lean knowledge base with dual (formal + informal) representation
  • A systematic comparison of GPT-5.4, Gemini 3.1 Pro, Claude Opus 4.7, and Claude Sonnet 4 on FormalMATH and two real PDE theorems across proving skills and autoformalization routes
  • A strict verification protocol (no sorry, non-empty proof, lake env lean acceptance) that corrects inflated raw pass rates

Results

  • FormalMATH subset (21 problems, 63 attempts per skill): NL-first achieves 20/63 (31.75%) vs. formalization-first 10/63 (15.87%), a doubling; per-model NL gains: +14.29% (Gemini 3.1 Pro, GPT-5.4), +19.05% (Claude Opus 4.7)
  • Domain sensitivity: NL-first gives large gains in Differentiation (0/9 → 6/9) and Precalculus (5/9 → 7/9); Integral, Other, and Sequences & Series remain 0/18 under both skills and all models
  • Recovery experiment (12 GPT-5.4-unsolved cases): MathCoPilot solves 9/12 on first pass; recursive blueprint refinement brings the total to 10/12
  • Real PDE theorems: Given a well-formed Lean formalization, Claude Opus 4.7 produces fully verified Lean 4 certificates on every attempt and GPT-5.4 follows closely; the same models fail on version-incompatible formalizations, demonstrating high sensitivity to autoformalization quality
  • Error detection: Performance on identifying errors in deliberately incorrect proofs varies sharply across models and skills (qualitative finding; specific numbers truncated in provided text)

Limitations

  • Undergraduate-level pass rates remain moderate (≤33%) even under the best skill; research-level PDE theorems are far harder
  • Performance is highly sensitive to Lean version compatibility in autoformalized statements — well-formed vs. incompatible formalizations produce near-perfect vs. near-zero success
  • Residual sorry is the dominant failure mode (19 instances under FF, 23 under NL), indicating models can plan proofs but cannot discharge Lean obligations for domains requiring substantial formal libraries
  • Entire theorem categories (Integral, Sequences & Series, Other) are unsolvable across all models and skills, pointing to missing formal infrastructure rather than model capability gaps
  • The knowledge base maintenance loop (re-verification on Mathlib updates) is automated but relies on the user to resolve flagged incompatibilities
  • Evaluation uses a small FormalMATH sample (21 problems across 7 domains, 3 per domain)

Relevance to Agentic AI / LLM Agents

MathCoPilot exemplifies a controlled human-in-the-loop multi-agent architecture where a fixed pipeline of specialized agents (Brainstorm, Blueprint, Prover, Formalizer, Aggregation) is orchestrated around a structured shared workspace rather than through unconstrained agent-to-agent dialogue — a design that directly addresses the controllability and interpretability challenges common in autonomous LLM agent systems. The adaptive skill orchestrator, which selects and switches strategies based on verifier feedback, is a concrete instance of feedback-driven tool-augmented agent planning. The finding that NL-first reasoning doubles strict formal verification rates has direct implications for LLM agent reasoning chains: intermediate informal representations improve grounded, verifiable downstream actions. For researchers tracking agentic AI, this work demonstrates the value of coupling symbolic verification environments (Lean 4) with LLM agents as an external correctness oracle, a pattern increasingly relevant to agent safety and reliability research.