lean_workbook_plus_30468

Proved

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

So we are left to prove: ${4(4n+3)(4n+1)\over 3(3n+2)(3n+1)} \leq 6^{\frac{1}{2}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30468 (n : ℕ) : (4 * (4 * n + 3) * (4 * n + 1) / (3 * (3 * n + 2) * (3 * n + 1))) ≤ Real.sqrt 6   :=  by sorry

Source