lean_workbook_plus_67836

Open

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

For each $n\in\mathbb{N}$ let $d_n$ denote the gcd of $n$ and $(2019-n)$ . Find value of $d_1+d_2+\cdots d_{2018}+d_{2019}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67836 : ∑ i in Finset.Icc 1 2019, Nat.gcd i (2019 - i) = 6725   :=  by sorry

Source