Prove2Me

lean_workbook_plus_16734

Disproved

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

By pqr pqr we have : p=2 p = 2 , q=1 q=1 , r≤427 r \le \frac{4}{27} ;

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16734 : ∀ p q r : ℝ, p = 2 ∧ q = 1 ∧ r ≤ 4 / 27   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph