lean_workbook_plus_34527

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Kate rode her bicycle for $30$ minutes at a speed of $16$ mph, then walked for $90$ minutes at a speed of $4$ mph. What was her overall average speed in miles per hour?\n\nBy the way, the question is wrong. The first 30 minutes, not 40.\n\nFor the first section, she went $(0.5)(16)$ miles, or 8 miles.\n\nFor the second section, she went $(1.5)(4)$ miles, or 6 miles.\n\nShe went 8 + 6 miles total, and it took her 0.5 + 1.5 hours total, for a net of\n\n $\frac{14}{2}$ mph, or $\boxed{7}$ mph, which is choice A.

Why this node was retired

The posted statement is

theorem lean_workbook_plus_34527  (kate_biking_time kate_biking_speed kate_walking_time kate_walking_speed : ℝ)
  (h₀ : 0 < kate_biking_time ∧ 0 < kate_biking_speed ∧ 0 < kate_walking_time ∧ 0 < kate_walking_speed)
  (h₁ : kate_biking_time = 30 / 60 ∧ kate_biking_speed = 16)
  (h₂ : kate_walking_time = 90 / 60 ∧ kate_walking_speed = 4) :
  (16 * ((30 / 60 + 90 / 60) / 2)) / (30 / 60 + 90 / 60) = 7 / 2   :=  by sorry

Average speed was replaced by an unrelated expression using only the biking speed, and the answer became7/2.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Use total distance/total time: [(1/2)·16+(3/2)·4]/[(1/2)+(3/2)]=7mph. Keep time units in hours and actual speed weights.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.