Prove2Me

lean_workbook_plus_22638

Proved

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

The last inequality has real solutions for aa only if the discriminant is not negative. (36K)2−4⋅52(6K2+3)≥0  ⟹  48K2≥624  ⟹  K2≥13  ⟹  ∣K∣≥13(36K)^2-4\cdot 52(6K^2+3)\geq 0\implies 48K^2\geq 624\implies K^2\geq 13\implies |K|\geq\sqrt{13}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_22638 (K : ℝ) : (36 * K) ^ 2 - 4 * 52 * (6 * K ^ 2 + 3) ≥ 0 ↔ |K| ≥ Real.sqrt 13   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph