lean_workbook_plus_66879

Proved

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

Prove that for $2/3 < x < 1$ , $\max \left \lbrace \frac{1-x}{1+3x}, \frac{3x^2-x-1}{3x} \right \rbrace < \frac{1}{3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66879 (x : ℝ) (hx1 : 2/3 < x) (hx2 : x < 1) : max ((1 - x) / (1 + 3 * x)) (3 * x ^ 2 - x - 1) / (3 * x) < 1 / 3   :=  by sorry

Source

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

View graph