lean_workbook_plus_41591

Proved

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

If the boats have been moving for time $t$ hours, then Boat A has moved $12t$ km while Boat B has moved $18t$ ; by Pythagoras, the distance between them is $\sqrt{(12t)^2+(18t)^2}=6\sqrt{13}t$ . Hence the rate of change of the distance between the boats is $\frac{6\sqrt{13}t}{t}=6\sqrt{13}\ \textrm{km}\,\textrm{h}^{-1}$ . This rate is constant, however long the boats have been travelling.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_41591  (t : ℝ)
  (h₀ : 0 < t) :
  Real.sqrt ((12 * t)^2 + (18 * t)^2) = 6 * Real.sqrt 13 * t   :=  by sorry

Source

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

View graph