Primary evidence
- An In-Context Learning Agent for Formal Theorem-ProvingS1 · Primary research · Paper · 2023-10-06
- COPRA repositoryS1 · Primary research · Repository
COPRA turns a general LLM into a stateful formal proof-search agent
At each step the agent proposed a tactic, executed it in the proof assistant, incorporated errors or new goals into the next prompt and maintained a search history for backtracking.
What happened?
COPRA used GPT-4 in a stateful backtracking loop with proof-environment feedback and retrieval, outperforming few-shot GPT-4 and reporting competitive results against finetuned provers on Lean miniF2F while also operating on Coq tasks.
At each step the agent proposed a tactic, executed it in the proof assistant, incorporated errors or new goals into the next prompt and maintained a search history for backtracking. The architecture showed how a frontier general model could be wrapped in a proof-oriented agent harness without task-specific finetuning.
Why it matters
COPRA made the proof assistant an interactive environment for an LLM agent, anticipating the generate-execute-observe-revise loop that later became central to formal mathematical agents.
Significance rationale: COPRA was an early explicit agentic theorem-proving design in which a general-purpose LLM repeatedly acted inside Lean or Coq, consumed proof-assistant feedback and backtracked through a maintained search state rather than answering in one shot.
Historical context
Earlier developments
Later developments
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Benchmark result
- Interface
- Formal, Symbolic, Hybrid
- AI contribution
- GPT-4 proposed tactics and navigated the proof search, while Lean or Coq checked each accepted proof action mechanically.
- Human contribution
- Researchers designed the agent state, retrieval, backtracking and prompting protocol, selected benchmarks and built the interfaces to the proof assistants.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- copra, gpt-4, lean, coq
- Organizations
- university-of-texas-at-austin
- Problems
- minif2f, compcert
- Methods
- agentic-proof-search, in-context-learning, backtracking, retrieval, proof-assistant-feedback
Sources & artifacts
- An In-Context Learning Agent for Formal Theorem-ProvingS1 · Primary research · Paper · accessed 2026-09-10
- COPRA repositoryS1 · Primary research · Repository · accessed 2026-09-10
- COPRA formal theorem-proving agentArtifact · Code
Verification history
- 2023-10-06 · Paper released · E2 · Research record
The authors released the paper describing the agent and its Lean and Coq evaluations.
- 2023-10-06 · Paper released · E3 · Inspectable artifact
Code and experiment infrastructure were made available in the public COPRA repository.
Corrections
No corrections recorded.