bibkey: oeis2024a373561 authors: OEIS Foundation Inc. year: 2024 title: OEIS A373561 doi: null url: https://oeis.org/A373561 claim: A comment on OEIS A373561 conjectures a closed form for a quadruple sum in which a greatest-common-divisor condition sorts the summands. strata_touched:
- D5/S3/Factorization/A373561 license: citation-only triage: anchor
OEIS A373561
The entry carries a conjectured closed form for a fourfold sum. Three indices
run over an initial interval and contribute the quantity x^2 + y^2 - z^2;
the fourth index selects, for each triple, only those whose greatest common
divisor with the modulus takes a prescribed value. Mats Granvik added the
statement on June 10, 2024, and the caller found it still labelled Conjecture
on September 9, 2026.
What the condition actually does
The divisor condition looks arithmetic but sorts rather than restricts. For a positive modulus the divisor of any summand with that modulus lies between one and the modulus, so every triple falls into exactly one class of the fourth index, and summing over all classes returns the original threefold sum. The quantity being summed can be zero or negative; the absolute value handles the sign, and a vanishing summand still lands in a legitimate class because the divisor of zero with the modulus is the modulus itself.
Once that layer is removed the identity is a square-sum computation: the two positive squares each contribute a full square sum scaled by the square of the interval length, and the negative square cancels one of them.
What the Lean module proves
D5/S3/Factorization/A373561 states the conjecture for every natural index,
including zero where both sides vanish. It is proved in the layers above:
the bucket collapse, the threefold reduction, their composition, and finally
the closed form. The last step multiplies through by six rather than dividing,
because the printed form has an integer division that truncates.
ASSUMED-UNVERIFIED: the identification of the printed sum with the module’s definition is a human reading of the entry, not a machine proof that the two denote the same quantity.
Search log
- Caller reading, 2026-09-09: the seat reported exact-phrase searches on the A-number alone and paired with the words proof, theorem, conjecture and Lean; semantic searches on the summand and on the printed closed form; a search restricted to arXiv; a search restricted to the public formal-conjectures repository; and the entry’s own revision history, where revision 17 records the conjecture’s addition and no later revision converts it to a theorem.
- The seat’s receipt is
所查来源未找到, explicitly not a claim that no proof exists anywhere. It also enumerated small cases itself and stated that this was a sanity check and not evidence of openness — the right distinction. - Caller verification, 2026-09-09: the orchestrator computed the fourfold sum by definition and checked the reduction claim independently before dispatching an implementation seat. Readings are in the problem entry.
Verified locator
- URL: https://oeis.org/A373561
- Square-sum sequence referenced by the entry: https://oeis.org/A000330