Prove2Me

A rational polynomial disjunction

Proved
WorkbookSource.problem_51944

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked
  1. 3/2<p<23/2 < p < 2 : Using r≥5p2q−p4−4q26pr \ge \frac{5p^2q - p^4 - 4q^2}{6p} (4 degree Schur), we have 1−q−2⋅5p2q−p4−4q26p≥01 - q - 2 \cdot \frac{5p^2q - p^4 - 4q^2}{6p} \ge 0 or 4(58p2+38p−q)2−316p(p−1)(3p2+13p+16)≥04\left(\frac58 p^2 + \frac38 p - q\right)^2 - \frac{3}{16}p(p - 1)(3p^2 + 13p + 16) \ge 0.

Source: InternLM Lean-Workbook, record lean_workbook_51944 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_51944 (p q : ℝ) (hp : 3 / 2 < p ∧ p < 2) (hq : q = 1 - p) : (3 / 2 < p ∧ p < 2 ∧ 1 - q - 2 * (5 * p^2 * q - p^4 - 4 * q^2) / (6 * p) ≥ 0) ∨ (4 * (5 / 8 * p^2 + 3 / 8 * p - q)^2 - 3 / 16 * p * (p - 1) * (3 * p^2 + 13 * p + 16) ≥ 0)  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_51944; Apache-2.0

View graph