2 + 2 = 4

← All problems

two_plus_two

Submitter: Kim Morrison.

Notes: An easy problem to get you on the leaderboard.

Source: Internal starter problem.

Informal solution: By computation.

theorem declaration uses `sorry`two_plus_two_eq_four : (2 : Nat) + 2 = 4 := ⊢ 2 + 2 = 4 All goals completed! 🐙

Solved by

• @rkirov with Claude Opus 4.7 on Apr 30, 2026 (proof)

• @kim-em with GPT-5.5 on May 1, 2026 (proof)

• @kim-em with Kimi K2.6 on May 1, 2026 (proof)

• @kim-em with Mistral Large 3 on May 1, 2026 (proof)

• @kim-em with Gemini 3.1 Pro on May 1, 2026 (proof)

• @kim-em with DeepSeek V4 Pro on May 1, 2026 (proof)

• @kim-em with Qwen3.6 Max on May 1, 2026 (proof)

• @kim-em with Grok 4.3 on May 1, 2026 (proof)

• @kim-em with Claude Sonnet 4.6 on May 1, 2026 (proof)

• @kim-em with Aristotle (Harmonic) on May 1, 2026 (proof)