Automated theorem proving—having computers generate formal mathematical proofs—has been a goal of AI since the 1950s. For decades, progress was slow: formal proofs require precise logical reasoning that neural networks were not designed for. The advent of large language models, trained on mathematical text and code, has changed the landscape dramatically. Systems like Goedel-Prover and Seed-Prover can now generate formal proofs in Lean (a proof assistant used by mathematicians) for problems ranging from undergraduate exercises to competition-level challenges.

The Research Landscape

Goedel-Prover: Open-Source SOTA

Lin and Lyu (2025), with 87 citations, introduce Goedel-Prover—an open-source language model that achieves state-of-the-art performance in automated formal proof generation. The key innovation addresses a fundamental bottleneck: the scarcity of formalized mathematical statements and proofs available for training.

Goedel-Prover solves this through a two-stage approach:

Statement formalization: An LLM translates informal mathematical statements (from textbooks, competitions, and research papers) into formal Lean statements, massively expanding the training data.

Proof generation: A second LLM, trained on the expanded dataset, generates formal proofs for the formalized statements.

The system achieves strong results on standard benchmarks: a 57.6% success rate (Pass@32) on MiniF2F (a challenging benchmark of competition-level mathematics), surpassing the previous leader DeepSeek-Prover-V1.5-RL by 7.6 percentage points. With additional RL training (including DPO), the success rate exceeds 60%. On PutnamBench (based on the William Lowell Putnam Mathematical Competition), Goedel-Prover solves 7 problems (Pass@512), ranking first on the leaderboard. Additionally, it provides formal proofs for 29,700 problems in Lean Workbook, nearly doubling the 15,700 solved by prior provers.

Seed-Prover: Reasoning Depth

Chen and Huang (2025), with 55 citations, take a complementary approach: rather than expanding training data, they improve the reasoning process itself. Seed-Prover uses reinforcement learning to develop long chain-of-thought reasoning—extended sequences of intermediate steps that build toward the final proof.

The insight is that formal theorem proving benefits from the same deep reasoning strategies that have improved LLM performance in mathematics and science (as demonstrated by DeepSeek R1 and OpenAI o1). By training the model to generate detailed proof sketches before attempting formal proof steps, Seed-Prover achieves higher success rates on difficult problems that require multi-step reasoning.

Human-AI Collaboration in Proving

Ospanov and Yousefzadeh (2025), with 11 citations, propose APOLLO—a system that combines LLM proof generation with Lean's verification capabilities in a collaborative loop. Rather than generating complete proofs in one pass, APOLLO iteratively generates proof attempts, receives feedback from the Lean proof checker, and refines its approach based on the feedback.

This interactive approach achieves higher proof rates than single-pass generation because it can recover from mistakes—a pattern familiar from human mathematical practice, where proofs are rarely correct on the first attempt.

Multi-Domain Proving

Del Tredici and Breen (2025), with 4 citations, extend theorem proving beyond pure mathematics into quantum physics. Their system, Ax-Prover, is a multi-agent framework where different agents specialize in different aspects of the proof process (formalization, lemma generation, proof search). The system can prove theorems involving quantum mechanics formalism—a domain with distinctive mathematical structures (Hilbert spaces, operators, bra-ket notation) that generic theorem provers handle poorly.

Critical Analysis: Claims and Evidence

<

Claim	Evidence	Verdict
LLMs can generate formal proofs at competition level	Goedel-Prover: 57.6% on MiniF2F (Pass@32), 7/644 (~1.1%) on PutnamBench (Pass@512)	✅ Supported — 87 citations; independently verified results
Deep reasoning (long chain-of-thought) improves theorem proving	Seed-Prover's RL-trained reasoning approach	✅ Supported — 55 citations
Interactive proof generation outperforms single-pass generation	APOLLO's iterative approach	✅ Supported — higher proof rates on difficult problems
LLM theorem proving extends to quantum physics	Ax-Prover's cross-domain demonstrations	⚠️ Uncertain — demonstrated on selected problems; generality untested

Open Questions

Understanding vs. pattern matching: Do LLM theorem provers "understand" mathematics, or do they pattern-match on proof structures? The philosophical question matters less than the practical one, but both are interesting.

Research-level mathematics: Current systems handle competition problems and textbook exercises. Can they contribute to research-level mathematics—proving novel theorems that humans have not yet proved?

Verification trust: Formal proofs generated by LLMs are verified by proof assistants (Lean, Coq). But do mathematicians trust and learn from these proofs?

Training data limits: Goedel-Prover's approach of translating informal mathematics into formal statements depends on the quality of the translation. Errors in formalization propagate to the proofs.

What This Means for Your Research

For mathematicians, LLM theorem provers are becoming practical research tools—not for replacing mathematical reasoning but for automating tedious proof steps and exploring proof strategies. For AI researchers, theorem proving is one of the cleanest benchmarks for reasoning capability—with objective verification through proof checkers.

Explore related work through ORAA ResearchBrain.

면책 조항: 이 게시물은 정보 제공 목적의 연구 동향 개요이다. 학술 작업에서 인용하기 전에 특정 발견, 통계 및 주장을 원본 논문과 대조하여 검증해야 한다.

Goedel-Prover와 자동화된 정리 증명에서의 LLM 혁명

자동화된 정리 증명—컴퓨터가 형식적인 수학적 증명을 생성하도록 하는 것—은 1950년대부터 AI의 목표였다. 수십 년간 진전은 더뎠다. 형식적 증명은 신경망이 설계된 방식과 맞지 않는 정밀한 논리적 추론을 요구하기 때문이다. 수학적 텍스트와 코드로 훈련된 대규모 언어 모델의 등장은 이 분야의 지형을 극적으로 변화시켰다. Goedel-Prover와 Seed-Prover 같은 시스템은 이제 수학자들이 사용하는 증명 보조 도구인 Lean에서 학부 수준의 연습 문제부터 경시대회 수준의 문제까지 다양한 형식적 증명을 생성할 수 있다.

연구 현황

Goedel-Prover: 오픈소스 SOTA

Lin and Lyu (2025)는 87회 인용으로, 자동화된 형식적 증명 생성에서 최첨단 성능을 달성하는 오픈소스 언어 모델인 Goedel-Prover를 소개한다. 핵심 혁신은 근본적인 병목 현상, 즉 훈련에 활용 가능한 형식화된 수학적 진술과 증명의 부족 문제를 해결하는 것이다.

Goedel-Prover는 2단계 접근 방식을 통해 이 문제를 해결한다:

진술 형식화: LLM이 교과서, 경시대회, 연구 논문에서 나온 비형식적인 수학적 진술을 형식적인 Lean 진술로 번역하여 훈련 데이터를 대폭 확장한다.

증명 생성: 확장된 데이터셋으로 훈련된 두 번째 LLM이 형식화된 진술에 대한 형식적 증명을 생성한다.

이 시스템은 표준 벤치마크에서 강력한 결과를 달성한다. 경시대회 수준 수학의 도전적인 벤치마크인 MiniF2F에서 57.6%의 성공률(Pass@32)을 기록하며 이전 선두였던 DeepSeek-Prover-V1.5-RL을 7.6 퍼센트 포인트 차이로 앞섰다. 추가적인 RL 훈련(DPO 포함)을 통해 성공률은 60%를 초과한다. William Lowell Putnam 수학 경시대회를 기반으로 한 PutnamBench에서는 Goedel-Prover가 7개 문제를 풀어(Pass@512) 리더보드 1위를 차지한다. 또한 Lean Workbook의 29,700개 문제에 대한 형식적 증명을 제공하여 이전 증명기들이 해결한 15,700개보다 거의 두 배에 달하는 수치를 기록한다.

Seed-Prover: 추론의 깊이

Chen and Huang (2025)는 55회 인용으로, 훈련 데이터를 확장하는 대신 추론 과정 자체를 개선하는 보완적 접근 방식을 취한다. Seed-Prover는 강화 학습을 사용하여 긴 연쇄적 추론(chain-of-thought reasoning)—최종 증명을 향해 쌓아가는 중간 단계들의 확장된 시퀀스—을 발전시킨다.

핵심 통찰은 형식적 정리 증명이 DeepSeek R1과 OpenAI o1에서 입증된 바와 같이 수학 및 과학 분야에서 LLM 성능을 향상시킨 것과 동일한 심층 추론 전략으로부터 이점을 얻는다는 것이다. 형식적 증명 단계를 시도하기 전에 상세한 증명 개요를 생성하도록 모델을 훈련시킴으로써, Seed-Prover는 다단계 추론을 요구하는 어려운 문제에서 더 높은 성공률을 달성한다.

증명에서의 인간-AI 협업

Ospanov and Yousefzadeh (2025)는 11회 인용으로, LLM 증명 생성과 Lean의 검증 기능을 협력적 루프로 결합한 시스템인 APOLLO를 제안한다. APOLLO는 완전한 증명을 한 번에 생성하는 대신, 증명 시도를 반복적으로 생성하고 Lean 증명 검사기로부터 피드백을 받아 그 피드백을 바탕으로 접근 방식을 개선한다.

이 상호작용적 접근 방식은 실수를 복구할 수 있기 때문에 단일 패스 생성보다 더 높은 증명 성공률을 달성한다. 이는 증명이 첫 번째 시도에서 거의 올바르지 않은 인간의 수학적 실천에서 익숙한 패턴이다.

다중 도메인 증명

Del Tredici와 Breen(2025)은 4회 인용으로, 정리 증명을 순수 수학을 넘어 양자 물리학 영역까지 확장한다. 이들의 시스템인 Ax-Prover는 다중 에이전트 프레임워크로, 각기 다른 에이전트가 증명 과정의 서로 다른 측면(형식화, 보조 정리 생성, 증명 탐색)을 전담한다. 이 시스템은 양자역학 형식론을 포함하는 정리를 증명할 수 있는데, 이 영역은 범용 정리 증명기가 잘 처리하지 못하는 독특한 수학적 구조(힐베르트 공간, 연산자, bra-ket 표기법)를 지닌다.

비판적 분석: 주장과 근거

<

주장	근거	판정
LLM이 경시대회 수준의 형식 증명을 생성할 수 있다	Goedel-Prover: MiniF2F에서 57.6% (Pass@32), PutnamBench에서 7/644 (~1.1%) (Pass@512)	✅ 지지됨 — 87회 인용; 독립적으로 검증된 결과
심층 추론(긴 chain-of-thought)이 정리 증명을 향상시킨다	Seed-Prover의 RL 기반 추론 접근법	✅ 지지됨 — 55회 인용
인터랙티브 증명 생성이 단일 패스 생성보다 성능이 우수하다	APOLLO의 반복적 접근법	✅ 지지됨 — 어려운 문제에서 더 높은 증명 성공률
LLM 정리 증명이 양자 물리학까지 확장된다	Ax-Prover의 교차 도메인 시연	⚠️ 불확실 — 선별된 문제에서 시연됨; 일반성 미검증

미해결 과제

이해 대 패턴 매칭: LLM 정리 증명기는 수학을 "이해"하는 것인가, 아니면 증명 구조에 대한 패턴 매칭을 수행하는 것인가? 이 철학적 질문은 실용적인 질문보다 덜 중요하지만, 두 가지 모두 흥미롭다.

연구 수준의 수학: 현재 시스템은 경시대회 문제와 교재 연습 문제를 다룬다. 인간이 아직 증명하지 못한 새로운 정리를 증명하는 등 연구 수준의 수학에 기여할 수 있는가?

검증에 대한 신뢰: LLM이 생성한 형식 증명은 증명 보조기(Lean, Coq)에 의해 검증된다. 그러나 수학자들은 이러한 증명을 신뢰하고 이로부터 학습하는가?

훈련 데이터의 한계: 비형식 수학을 형식 명제로 번역하는 Goedel-Prover의 접근법은 번역의 품질에 의존한다. 형식화 과정의 오류는 증명에도 전파된다.

연구에 주는 시사점

수학자들에게 LLM 정리 증명기는 실용적인 연구 도구로 자리잡고 있다—수학적 추론을 대체하기 위해서가 아니라, 반복적인 증명 단계를 자동화하고 증명 전략을 탐색하기 위해서이다. AI 연구자들에게 정리 증명은 추론 능력을 위한 가장 명확한 벤치마크 중 하나로, 증명 검사기를 통한 객관적 검증이 가능하다.

ORAA ResearchBrain을 통해 관련 연구를 탐색할 수 있다.