Prove2Me

lean_workbook_plus_66500

Proved

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

Show that there does not exist an infinite set MM of distinct positive integers such that for all a≠b∈Ma \neq b \in M, (a−b)2∣ab(a - b)^2 | ab.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66500 (M : Set ℕ) (hM : M.Infinite) (hM' : M.PairwiseDisjoint fun (a : ℕ) (b : ℕ) ↦ (a - b)^2 ∣ a * b) : False   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph