lean_workbook_plus_25110

Disproved

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

$x^{3}\equiv 0 \vee \pm 1 \mod 7 \implies x^{3}+y^{3}+z^{3}\not \equiv 1969^{2}\mod 7$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25110 : ∀ x y z : ℤ, (x^3 ≡ 0 [ZMOD 7] ∨ x^3 ≡ 1 [ZMOD 7] ∨ x^3 ≡ -1 [ZMOD 7]) → ¬(x^3 + y^3 + z^3 ≡ 1969^2 [ZMOD 7])   :=  by sorry

Source

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

View graph