lean_workbook_plus_28871
ProvedNote that is always even for all integers . Similarly, and are also always even. Therefore, their sum, , must also be even. However, is not an even number, so there are no integer solutions.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28871 : ∀ x y z : ℤ, Even (x * y * (x ^ 2 - y ^ 2) + y * z * (y ^ 2 - z ^ 2) + z * x * (z ^ 2 - x ^ 2)) := by sorry
Source