Prove2Me

Lean-Workbook Syntax 67836: A finite sum of gcd values

Proved
WorkbookSyntax.plus_67836

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

∑i=12019gcd⁡(i,2019−i)=6725\sum_{i=1}^{2019}\gcd(i,2019-i)=6725.

Source: Lean-Workbook row lean_workbook_plus_67836 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble
import Mathlib.Algebra.BigOperators.Intervals
Formal statement
theorem WorkbookSyntax.plus_67836 : ∑ i ∈ Finset.Icc 1 2019, Nat.gcd i (2019 - i) = 6725   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_67836; immutable original Prove2Me node 4b0ea5bd-bcfb-45ac-8bed-12b0046e9e67

View graph