lean_workbook_plus_16326

Disproved

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

Express $\frac{118}{7}t^4+8t^3+12t^2+8t+\frac{10}{7}$ as $\left(\frac{6}{7}t^4-\frac{1}{4}t^2+\frac{1}{50}\right)+\left(4t^2+t-\frac{3}{25}\right)^2+\left(\frac{1221}{100}t^2+\frac{206}{25}t+\frac{493}{350}\right)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16326 (t : ℝ) : (118 / 7 * t ^ 4 + 8 * t ^ 3 + 12 * t ^ 2 + 8 * t + 10 / 7) = (6 / 7 * t ^ 4 - 1 / 4 * t ^ 2 + 1 / 50) + (4 * t ^ 2 + t - 3 / 25) ^ 2 + (1221 / 100 * t ^ 2 + 206 / 25 * t + 493 / 350)   :=  by sorry

Source

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

View graph