Terminal-Bench 2.1terminalCoq
Complete a Coq proof of addition commutativity
Fill the missing inductive proof steps for natural-number addition commutativity and compile the verified theorem.
prove-plus-comm
Normalized profile
What this task asks for
Fill the missing inductive proof steps for natural-number addition commutativity and compile the verified theorem. Prove forall n m : nat, n + m = m + n. Complete the existing induction-based argument. Compile successfully with coqc.
Intent
- bug repair
- test and validation
Work surfaces
- formal proof
- proof compiler
Technology
- Coq
Expected artifacts
- completed plus_comm.v
- plus_comm.vo
What makes it difficult
- native compilation and dependency integration
Published evidence
Model × harness outcomes
Counts are tied to these exact configurations. Harnesses are not treated as equivalent across benchmarks.
- Models
- 13
- Configurations
- 20
- Trials
- 100
Showing 20 of 20 configurations
| Model | Harness | Effort | Result | Passes |
|---|---|---|---|---|
| claude-fable-5anthropic · 2026-06-07 | claude-code2.1.167 | xhigh | All passed | 5/5 |
| claude-fable-5anthropic · 2026-06-05 | terminus-22.0.0 | high | All passed | 5/5 |
| claude-opus-4-7anthropic · 2026-05-01 | claude-code2.1.123 | max | All passed | 5/5 |
| claude-opus-4-7anthropic · 2026-05-01 | terminus-22.0.0 | max | All passed | 5/5 |
| claude-opus-4-8anthropic · 2026-07-09 | claude-code2.1.205 | high | All passed | 5/5 |
| claude-sonnet-5anthropic · 2026-07-09 | claude-code2.1.205 | high | All passed | 5/5 |
| gemini-3-pro-previewgemini · 2026-05-01 | gemini-cli0.40.0 | high | All passed | 5/5 |
| gemini-3-pro-previewgemini · 2026-05-01 | terminus-22.0.0 | high | All passed | 5/5 |
| gemini-3.1-pro-previewgemini · 2026-05-05 | gemini-cli0.40.0 | high | Mixed1 errors | 4/5 |
| gemini-3.1-pro-previewgemini · 2026-05-05 | terminus-22.0.0 | high | All passed | 5/5 |
| glm-5.1zai · 2026-05-01 | claude-code2.1.123 | max | All passed | 5/5 |
| gpt-5.5openai · 2026-05-01 | codex0.125.0 | xhigh | All passed | 5/5 |
| gpt-5.5openai · 2026-05-01 | terminus-22.0.0 | xhigh | All passed | 5/5 |
| gpt-5.6-lunaopenai · 2026-07-10 | codex0.144.0 | max | All passed | 5/5 |
| gpt-5.6-lunaopenai · 2026-07-11 | codex0.144.1 | max | All passed | 5/5 |
| gpt-5.6-solopenai · 2026-07-10 | codex0.144.0 | max | All passed | 5/5 |
| gpt-5.6-terraopenai · 2026-07-10 | codex0.144.0 | max | All passed | 5/5 |
| gpt-5.6-terraopenai · 2026-07-11 | codex0.144.1 | max | All passed | 5/5 |
| grok-4.5cursor · 2026-07-09 | cursor-cli2026.07.08-0c04a8a | default | All passed | 5/5 |
| muse-spark-1.1openai · 2026-07-09 | mini-swe-agent2.4.5 | xhigh | All passed | 5/5 |