lean_workbook_plus_46631

Disproved

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

Prove that $9^3(a^4+1)^3(b^4+1)^3(c^4+1)^3\geq 8^3(a^6+a^3+1)^2(b^6+b^3+1)^2(c^6+c^3+1)^2\geq 8^3(a^2b^2c^2+abc+1)^6$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46631 : ∀ a b c : ℝ, 9^3 * (a^4 + 1)^3 * (b^4 + 1)^3 * (c^4 + 1)^3 ≥ 8^3 * (a^6 + a^3 + 1)^2 * (b^6 + b^3 + 1)^2 * (c^6 + c^3 + 1)^2 ∧ 8^3 * (a^6 + a^3 + 1)^2 * (b^6 + b^3 + 1)^2 * (c^6 + c^3 + 1)^2 >= 8^3 * (a^2 * b^2 * c^2 + a * b * c + 1)^6   :=  by sorry

Source

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

View graph