Prove2Me

Factoring the absolute difference of quadratic values

Proved
WorkbookSource.base_32959

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

lean-workbooksource-checked

Simplify ∣3x2+4−3k2−4∣=3∣x−k∣∣x+k∣|3x^2 + 4 - 3k^2 - 4| = 3|x - k||x + k|

Source: InternLM Lean-Workbook, record lean_workbook_32959 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_32959 (x k : ℝ) : ‖3 * x ^ 2 + 4 - (3 * k ^ 2 + 4)‖ = 3 * ‖x - k‖ * ‖x + k‖  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_32959; Apache-2.0

View graph