lean_workbook_plus_702

Proved

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

In fact, if $A,B,C$ are pairwise relatively prime, then the equation $x^A+y^B=z^C$ has infinitely many solutions where $x,y,z$ are positive integers.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_702 (A B C : ℕ) (hA : A ≠ 0) (hB : B ≠ 0) (hC : C ≠ 0) (hABC : Nat.Coprime A B) (hABC' : Nat.Coprime A C) (hABC'' : Nat.Coprime B C) : ∃ x y z : ℕ, x^A + y^B = z^C   :=  by sorry

Source

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

View graph