Prove2Me

The minimum squared distance under a shifted product constraint

Proved
WorkbookCorrected.plus_21177

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

corrected-formalizationlean-workbooksource-checked

For real numbers x,yx,y satisfying (x+1)(y+1)=9(x+1)(y+1)=9, the minimum of x2+y2x^2+y^2 is 88, attained at (x,y)=(2,2)(x,y)=(2,2).

Formalization Note: The original source asks for an extremum, while its formal statement supplied only a bound. This complete formulation includes both the universal bound and existence of an attaining point.

Source: InternLM Lean-Workbook, record lean_workbook_plus_21177 (Apache-2.0).

Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_21177 : (∀ x y : ℝ, (x+1)*(y+1)=9 → 8 ≤ x^2+y^2) ∧
    (∃ x y : ℝ, (x+1)*(y+1)=9 ∧ x^2+y^2=8) := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_21177; Apache-2.0

View graph