lean_workbook_plus_35207

Proved

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

So now we minimize $[CMN]+[APB]$ . Let $CN=x$ and the side length of the equilateral be $1$ . So the area we want to minimize is equal to $\frac{\sqrt{3}}{4}x^2+\frac{\sqrt{3}}{4}(1-x)=\frac{\sqrt{3}}{4}(x^2-x+1)=\frac{\sqrt{3}}{4}((x-\frac{1}{2})^2+\frac{3}{4})$ . The minimum value of this is $\frac{3\sqrt{3}}{16}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35207  (x : ℝ)
  (h₀ : 0 < x)
  (h₁ : x ≤ 1) :
  3 * Real.sqrt 3 / 16 ≤ x^2 * Real.sqrt 3 / 4 + (1 - x) * Real.sqrt 3 / 4   :=  by sorry

Source

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

View graph