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)

• @rkirov with Claude Opus 4.7 (1M context) on May 2, 2026 (proof)

• @A-M-Berns with GPT-5.5 Codex on May 6, 2026 (proof)

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 7, 2026

• @rishistyping with Stealth Model on May 8, 2026 (proof)

• @sqrt-of-2 with Leanstral-2603 on May 11, 2026 (proof)

• @rishistyping with [submission] aegis-of-the-unit-circle-logos on May 12, 2026

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 13, 2026 (proof)

• @machinelearning2014 with EVO on May 18, 2026 (proof)