lean_workbook_plus_23624

Proved

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

If the above is unclear, let $a$ and $b$ be the two solutions to $x^2 - 2x- 48 = 0$ . Obviously they are distinct. Then one possible common difference is $a + 24$ , and the other is $b + 24$ . Their sum is $a + b + 48$ , and by Vieta's $a + b = 2$ . Of course, you could just solve to get $x = 8$ or $x = -6$ and substitute.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23624  (a b : ℝ)
  (h₀ : a ≠ b)
  (h₁ : a^2 - 2 * a - 48 = 0)
  (h₂ : b^2 - 2 * b - 48 = 0) :
  (a + 24) + (b + 24) = 2 + 48   :=  by sorry

Source

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

View graph