Prove2Me

lean_workbook_plus_1003

Proved

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

SolutionIdeally, abc−def=1abc-def=1 . Guessing and checking without using 99 or 88 in the numerator gives frac6⋅3⋅2−7⋅5⋅19⋅8⋅4\\frac{6\cdot3\cdot2-7\cdot5\cdot1}{9\cdot8\cdot4} . Since abc−def=1abc-def=1 , then one of {a,b,c}\{a,b,c\} or {d,e,f}\{d,e,f\} must contain only odd factors, and trying the 1,3,51,3,5 case means one of them must be 77 or 99 . As well, it's impossible to get frac19⋅8⋅6\\frac{1}{9\cdot8\cdot6} by checking all of the cases, leaving frac6⋅3⋅2−7⋅5⋅19⋅8⋅4=1288\\frac{6\cdot3\cdot2-7\cdot5\cdot1}{9\cdot8\cdot4}=\frac{1}{288} as the minimum positive fraction achievable, for an answer of 289\boxed{289} .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1003  (a b c d e f : ℕ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ 0 < e ∧ 0 < f)
  (h₁ : a * b * c - d * e * f = 1) :
  (a * b * c - d * e * f : ℚ) ≥ 1 / 288   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph