Prove2Me

lean_workbook_plus_81217

Proved

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

x≤13→1≥x3 x\le \frac{1}{\sqrt 3} \to 1 \ge x\sqrt 3

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_81217 (x : ℝ) (hx : x ≤ 1 / Real.sqrt 3) : 1 ≥ x * Real.sqrt 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph