lean_workbook_plus_45680

Disproved

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

squaring $u^2v^2(10u^3-8uv^2)^2(9u^2-8v^2)\\leq 81u^{12}+306u^{10}v^2-431u^8v^4-1072u^6v^6+2144u^4v^2-1280u^2v^{10}+256v^{12}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45680 : ∀ u v : ℝ, (u^2 * v^2 * (10 * u^3 - 8 * u * v^2)^2 * (9 * u^2 - 8 * v^2)) ≤ (81 * u^12 + 306 * u^10 * v^2 - 431 * u^8 * v^4 - 1072 * u^6 * v^6 + 2144 * u^4 * v^2 - 1280 * u^2 * v^10 + 256 * v^12)   :=  by sorry

Source

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

View graph