lean_workbook_plus_22280

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

First, we bound $n$ . Note that for $n\geq3$ , $n^k < n^k+n^m < n^{k+1}$ for $m\leq k$ . Thus, $n\leq 2$ . Furthermore, letting $n=1$ gives $1^a+1^b=1^c\to1+1=1$ , a contradiction. Thus, $n=2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_22280  (n k m a b c : ℕ)
  (h₀ : 0 < n ∧ 0 < k ∧ 0 < m ∧ 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : n^k + n^m = n^a + n^b + n^c)
  (h₂ : k ≤ a ∧ m ≤ b ∧ c ≤ k)
  (h₃ : n ≤ 2) :
  n = 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph