Prove2Me

lean_workbook_plus_81282

Proved

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

Let x=abc‾x=\overline{abc}, and the problem is 1000x+(1000−x)=y21000x+(1000-x)=y^2 with x,y∈[100,1000)x,y\in[100,1000) So 999(x+1)=y2−1999(x+1)=y^2-1 and so we have to solve (without computer) y2≡1(mod27×37)y^2\equiv 1\pmod{27\times 37}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_81282 (x y : ℕ) (hx : 100 ≤ x ∧ x ≤ 1000) (hy : 100 ≤ y ∧ y ≤ 1000) (h : 1000 * x + (1000 - x) = y ^ 2) : 999 * (x + 1) ≡ 0 [ZMOD 27 * 37]   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph