Prove2Me

lean_workbook_plus_671

Disproved

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

1k2x2+x(1k4−1−1k2−1k3−1k(k2+1))+(1k2+1k3−1k4−1k)≤0 \frac {1}{k^2}x^2 + x\left(\frac {1}{k^4} - 1 - \frac {1}{k^2} - \frac {1}{k^3} -\frac {1}{k(k^2 + 1)} \right) + \left(\frac {1}{k^2} + \frac {1}{k^3} - \frac {1}{k^4} - \frac {1}{k}\right)\leq 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_671 : ∀ k : ℝ, k > 0 → ∀ x : ℝ, 1 / k ^ 2 * x ^ 2 + x * (1 / k ^ 4 - 1 - 1 / k ^ 2 - 1 / k ^ 3 - 1 / (k * (k ^ 2 + 1))) + (1 / k ^ 2 + 1 / k ^ 3 - 1 / k ^ 4 - 1 / k) ≤ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph