Formal theorem proving on PhysLeanData (test)
58.8Classical ScorePhysProver
Evaluation results
| Method | Links | |||||
|---|---|---|---|---|---|---|
| PhysProverBackbone=DeepSeek-Prover-V2-7B, Training Technique=GRPO (RL) with rule-based rewards, Lean Version=4.20.02026.01 | 58.8 | 26.9 | 39.3 | 26.8 | 36.4 | |
| Deepseek-Prover-V2-7BModel Type=Open-source Formal Math Prover, Training=None (zero-shot/baseline)2026.01 | 54.9 | 23.9 | 37.7 | 25.4 | 34 | |
| Claude-4.5-SonnetModel Type=Proprietary, Reasoning Mode=Chain-of-Thought (CoT)2026.01 | 52.9 | 19.4 | 29.5 | 39.4 | 34.4 | |
| Goedel-Prover-V2-8BModel Type=Open-source Formal Math Prover, Training=None (zero-shot/baseline)2026.01 | 49 | 19.4 | 34.4 | 28.2 | 31.6 | |
| GPT-5Model Type=Proprietary, Reasoning Mode=Chain-of-Thought (CoT)2026.01 | 37.3 | 13.4 | 21.3 | 35.2 | 26.4 | |
| Kimina-Prover-Distill-8BModel Type=Open-source Formal Math Prover, Training=None (zero-shot/baseline)2026.01 | 35.3 | 14.9 | 29.5 | 22.5 | 24.8 |