Theorem Proving on ProverBench
5.5Proof LengthClaude 4.6 Opus
Evaluation results
| Method | Links | |
|---|---|---|
| Claude 4.6 OpusType=Proprietary LLM2026.04 | 5.5 | |
| Gemini 3.1 ProType=Proprietary LLM2026.04 | 6.6 | |
| Gemini 2.5 ProType=Proprietary LLM2026.04 | 12.7 | |
| GPT-5.3-CodexType=Proprietary LLM2026.04 | 12.8 | |
| DeepSeek-Prover-V2-7BType=Open-source LLM2026.04 | 19.6 | |
| Goedel-Prover-V2-8BType=Open-source LLM2026.04 | 21.7 | |
| DreamProverBackbone=GPT-5.3-Codex, Type=Lemma Learning System2026.04 | 34.1 | |
| Goedel-Prover-V2-32BType=Open-source LLM2026.04 | 41.8 | |
| DreamProverBackbone=Gemini 2.5 Pro, Type=Lemma Learning System2026.04 | 41.8 | |
| HilbertBackbone=Gemini 2.5 Pro, Type=Agentic System2026.04 | 45.8 | |
| DreamProverBackbone=Gemini 3.1 Pro, Type=Lemma Learning System2026.04 | 51.7 | |
| HilbertBackbone=Gemini 3.1 Pro, Type=Agentic System2026.04 | 65.7 | |
| HilbertBackbone=GPT-5.3-Codex, Type=Agentic System2026.04 | 67.3 |