lean_workbook_plus_72787

Proved

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

We can solve these problems using the formula for harmonic mean, $\frac{2}{\frac{1}{a}+\frac{1}{b}} = 30$ . Let $x$ be the number of minutes that Bertha uses. We already have one rate, so we solve for the second. \n\n $\frac{2}{\frac{1}{40}+\frac{1}{b}} = 30$ \n\n $\frac{80b}{b+40} = 30$ \n\n $80b = 30b+1200$ \n\n $50b = 1200$ \n\n $b = 24$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72787  (b : ℝ)
  (h₀ : 0 < b)
  (h₁ : 2 / (1 / 40 + 1 / b) = 30) :
  b = 24   :=  by sorry

Source

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

View graph