lean_workbook_plus_9331

Proved

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

Evaluate $A = \dfrac{2020}{1+\dfrac{2017}{2018} + \dfrac{2017}{2019}} + \dfrac{2020} {1+\dfrac{2018}{2017} + \dfrac{2018}{2019}} \ + \dfrac{2020}{1+\dfrac{2019}{2017} + \dfrac{2019}{2018}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9331 (A : ℝ) : A = 2020 / (1 + 2017 / 2018 + 2017 / 2019) + 2020 / (1 + 2018 / 2017 + 2018 / 2019) + 2020 / (1 + 2019 / 2017 + 2019 / 2018) → A = 2020   :=  by sorry

Source

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

View graph