lean_workbook_plus_12050

Proved

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

We can have Anita be $y$ and Basilio be $x$ . The equations are $y=4.5+x$ and $6x+3y=36$ . Solving these equations is $x=2.5$ and $y=7$ . Therefore, Anita is 7 years old and Basilio is 4.5 years old.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12050 (x y : ℝ) (h₁ : y = 4.5 + x) (h₂ : 6 * x + 3 * y = 36) : y = 7 ∧ x = 2.5   :=  by sorry

Source

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

View graph