lean_workbook_plus_68393

Proved

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

Find the value of $abc$ where $a = \frac{1999\cdot1999-1999}{1998\cdot1998+1998}$ , $b = \frac{2000\cdot2000-2000}{1999\cdot1999+1999}$ , and $c = \frac{2001\cdot2001-2001}{2000\cdot2000+2000}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68393 (a b c : ℚ) (ha : a = (1999 * 1999 - 1999) / (1998 * 1998 + 1998)) (hb : b = (2000 * 2000 - 2000) / (1999 * 1999 + 1999)) (hc : c = (2001 * 2001 - 2001) / (2000 * 2000 + 2000)) : a * b * c = 1   :=  by sorry

Source

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

View graph