lean_workbook_plus_2977

Proved

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

Let's say Harry is $h$ years old. Then Tom's age is $2h/3$ . Hence $h-2h/3 = 666$ , so $h=\boxed {1998}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2977  (h : ℝ)
  (h₀ : h - 2 * h / 3 = 666) :
  h = 1998   :=  by sorry

Source