lean_workbook_plus_59249

Disproved

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

$s\geq 2\,r+\sqrt {3\,{r}^{2}-3\,\sqrt {3}{R}^{2}-2\,Rr+8\,{R}^{2}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59249 : ∀ (s : ℝ) (r : ℝ) (R : ℝ), s ≥ 2 * r + Real.sqrt (3 * r^2 - 3 * Real.sqrt 3 * R^2 - 2 * R * r + 8 * R^2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph