Prove2Me

A quadratic norm minimum under three pair-product constraints

Proved
WorkbookCorrected.base_709

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

corrected-formalizationlean-workbooksource-checked

Let a, b, ca,\ b,\ c and dd be real numbers such that

{(a+b)(c+d)=2 (a+c)(b+d)=3 (a+d)(b+c)=4\begin{cases} (a+b)(c+d)=2 \ (a+c)(b+d)=3 \ (a+d)(b+c)=4 \end{cases}

Find the minimum possible value of the expression

a2+b2+c2+d2.a^2+b^2+c^2+d^2.

Source: InternLM Lean-Workbook, record lean_workbook_709 (Apache-2.0). Natural-language proposition preserved; the source bound is completed with an exact attainment witness. Proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookCorrected.base_709 : (∀ (a b c d : ℝ) (h1 : (a + b) * (c + d) = 2) (h2 : (a + c) * (b + d) = 3) (h3 : (a + d) * (b + c) = 4), 7 ≤ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) ∧ (∃ a b c d : ℝ, ((a + b) * (c + d) = 2) ∧ ((a + c) * (b + d) = 3) ∧ ((a + d) * (b + c) = 4) ∧ ( 7  =  a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2  )) := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_709; Apache-2.0

View graph