lean_workbook_plus_35005

Proved

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

Given that $(x, y)$ satisfies $x^2+y^2=9$ , what is the largest possible value of $x^2 + 3y^2 + 4x$ ? (For this problem I solved for $y$ in the first equation and plugged it back in the second to get 29. What other way can this be done?)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35005 (x y : ℝ) (hx : x^2 + y^2 = 9) : x^2 + 3*y^2 + 4*x ≤ 29   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph