Prove2Me

lean_workbook_plus_43169

Proved

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

Call the side length of the squares aa , we then have the inequality: \n\n (52a−1)×24+(24a−1)×52≤1994\displaystyle \left(\frac{52}{a} - 1 \right) \times 24 + \displaystyle \left(\frac{24}{a} - 1 \right) \times 52 \leq 1994 \n\n Simplifying the inequality, we have: \n\n a≥416345a \geq \frac{416}{345}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43169  (a : ℝ)
  (h₀ : 0 < a)
  (h₁ : (↑52 / a - 1) * 24 + (↑24 / a - 1) * 52 ≤ 1994) :
  a ≥ 416 / 345   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph