Prove2Me

lean_workbook_plus_20026

Proved

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

If x,yx,y are positive integers and x3+y3=x2+y2 x^3 + y^3 = x^2 + y^2 , then x=y=1x=y=1 and so xy=1xy=1\nBecause x2+y2=x3+y3≥xy(x+y)=x2y+y2x⇒x2(1−y)+y2(1−x)=0⇒x=y=1x^2+y^2=x^3+y^3\geq xy(x+y)=x^2y+y^2x\Rightarrow x^2(1-y)+y^2(1-x)=0 \Rightarrow x=y=1

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20026  (x y : ℕ)
  (h₀ : 0 < x ∧ 0 < y)
  (h₁ : x^3 + y^3 = x^2 + y^2) :
  x = y ∧ x = 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph