A linear maximum on a shifted ellipse

Proved

WorkbookCorrected.base_29209

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

corrected-formalizationlean-workbooksource-checked

Find the max. value of $(4x-9y)/2$ if $x^2+9y^2-4x+6y+4=0$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookCorrected.base_29209 : (∀ x y : ℝ, x^2 + 9*y^2 - 4*x + 6*y + 4 = 0 → (4*x - 9*y)/2 ≤ 8) ∧ (∃ x y : ℝ, x^2 + 9*y^2 - 4*x + 6*y + 4 = 0 ∧ (4*x - 9*y)/2 = 8) := by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_29209; Apache-2.0

View graph