lean_workbook_plus_63758

Proved

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

$S < 2\cdot\frac{1}{2\sqrt3} +\frac{1/3}{(1/3)^{2}+3}<\frac{3}{4}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63758 : (1 / 2 * (1 / Real.sqrt 3) + (1 / 3) / ((1 / 3) ^ 2 + 3)) < (3:ℝ) / 4   :=  by sorry

Source