lean_workbook_plus_64102

Disproved

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

Let $x$ be the number of hours it would take the men to meet. \n\n Then we get the distance $4x$ for the $M$ man and $\frac{x}{2}[4+\frac{x-1}{2}]$ for the second man. They travel a total of 72 miles together when they meet. So we have the equation \n\n $4x+\frac{x}{2}[4+\frac{x-1}{2}]=72$ \n\n $4x+2x+\frac{1}{4}x^2-\frac{1}{4}x=72$ \n\n $6x+\frac{1}{4}x^2-\frac{1}{4}x=72$ \n\n $x^2-x+24=72$ \n\n $x^2-x-48=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64102  (x : ℝ)
  (h₀ : 0 < x)
  (h₁ : 4 * x + (x / 2) * (4 + (x - 1) / 2) = 72) :
  x^2 - x - 48 = 0   :=  by sorry

Source

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

View graph