lean_workbook_plus_17787

Disproved

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

Let the height of the lamp be $z$ . Then, using the man's height and length of shadow, we have the ratio $\frac{z}{x}=\frac{1.8}{6.5} \Rightarrow\frac{z}{20}=\frac{1.8}{6.5}$ , and we get $z=5.5$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17787  (z x : ℝ)
  (h₀ : 0 < z ∧ 0 < x)
  (h₁ : z / x = 1.8 / 6.5)
  (h₂ : x = 20) :
  z = 5.5   :=  by sorry

Source

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

View graph