lean_workbook_plus_2623

Proved

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

Prove that for all distinct integers $x, y, z$ , $5(x-y)(y-z)(z-x)$ divides $(x-y)^5+(y-z)^5+(z-x)^5$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2623 (x y z : ℤ) (hxy : x ≠ y) (hyz : y ≠ z) (hxz : x ≠ z) : 5 * (x - y) * (y - z) * (z - x) ∣ (x - y) ^ 5 + (y - z) ^ 5 + (z - x) ^ 5   :=  by sorry

Source

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

View graph