Formal Theorem Proving on Inequality
3.1567NEQHilbert
Evaluation results
| Method | Links | |||
|---|---|---|---|---|
| HilbertBackbone=Gemini 3.1 Pro, System=Agentic System2026.04 | 3.1 | 1.28 | 2.92 | |
| HilbertBackbone=Gemini 2.5 Pro, System=Agentic System2026.04 | 2.86 | 1.48 | 3.4 | |
| Goedel-Prover-V2-32BType=Open-source LLM2026.04 | 1.52 | 0.79 | 1.07 | |
| Goedel-Prover-V2-8BType=Open-source LLM2026.04 | 1.44 | 0.61 | 0.82 | |
| DreamProverBackbone=Gemini 3.1 Pro, System=Lemma Learning System2026.04 | 1.3 | 1.47 | 0.92 | |
| DreamProverBackbone=Gemini 2.5 Pro, System=Lemma Learning System2026.04 | 1.12 | 1.39 | 1.2 | |
| Gemini 2.5 ProType=Proprietary LLM2026.04 | 0.81 | 0.65 | 0.68 | |
| HilbertBackbone=GPT-5.3-Codex, System=Agentic System2026.04 | 0.78 | 0.52 | 0.96 | |
| Gemini 3.1 ProType=Proprietary LLM2026.04 | 0.62 | 0.68 | 0.76 | |
| DreamProverBackbone=GPT-5.3-Codex, System=Lemma Learning System2026.04 | 0.53 | 0.68 | 0.5 | |
| Claude 4.6 OpusType=Proprietary LLM2026.04 | 0.51 | 0.47 | 0.52 | |
| DeepSeek-Prover-V2-7BType=Open-source LLM2026.04 | 0.38 | 0.33 | 0.36 | |
| GPT-5.3-CodexType=Proprietary LLM2026.04 | 0.28 | 0.24 | 0.3 |