lean_workbook_plus_6627

Proved

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

If they're arranged in a $2\times2$ grid, then we maximize $xy$ given $3x+3y=120$ , or $x+y=40$ . At $x=y=20$ , this gives us $\boxed{400}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6627  (x y : ℝ)
  (h₀ : 0 < x ∧ 0 < y)
  (h₁ : 3 * x + 3 * y = 120)
  (h₂ : x + y = 40) :
  x * y ≤ 400   :=  by sorry

Source