Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

bibkey: eldar2019a025529 authors: Amiram Eldar; Thomas Ordowski; OEIS Foundation Inc. year: 2019 title: “OEIS A025529: the LCM-weighted harmonic sum and composite-solution conjecture” doi: null url: https://oeis.org/A025529 claim: “The sequence is the LCM-weighted harmonic sum. The August 7, 2019 comment conjectures that composite n dividing a(n-1) are only squares of primes greater than three.” strata_touched:

  • D5/S3/ArithSums/A025529PrimeCubeRefutation license: citation-only triage: anchor

OEIS A025529

The NAME defines a(n) as (1/1 + 1/2 + … + 1/n) times lcm{1,…,n}. Thomas Ordowski’s August 7, 2019 FORMULA gives the equal exact-quotient sum Sum_{k=1..n} lcm(1,…,n)/k. The sequence starts at n=1; the formal representation extends it by the empty-sum convention A(0)=0.

The COMMENT by Amiram Eldar and Thomas Ordowski, August 7, 2019, states:

It seems that composite numbers n such that n | a(n-1) are only the squares n = p^2 of primes p > 3.

The claim is cited as a conjecture, not as an established theorem. The formal refutation uses the prime cube 16843^3 and a structural harmonic congruence argument. The neighboring conjecture about n^2 dividing a(n-1) is a different statement.

Verified locator

  • Entry: https://oeis.org/A025529 , revision 99, February 10, 2026.
  • Immutable official mirror: https://github.com/oeis/oeisdata/blob/69b127f67c75990effad199e316d6e8a5183b64c/seq/A025/A025529.seq
  • Fields: NAME, the Eldar–Ordowski August 7, 2019 COMMENT, and Ordowski’s same-day FORMULA.

The Epoch results submission for A064169 contains Wolf.p16843_prime and Wolf.val_harmonic_16842, respectively primality of 16843 and (3 : ℤ) ≤ padicValRat 16843 (harmonic 16842). These are relevant finite premises; that submission’s A064169 endpoint is a different claim. The exact source is Submission/Spec.lean, SHA256 57f18ba88858609adfd9fc0a0afdb6f6c4e1795dde4670957bda175631377304.

Redistribution permission for the added Wolf proofs is not established by that results repository or its linked source chain. The linked methodology LICENSE grants MIT terms for that project and retains Apache-2.0 notices for its Formal Conjectures inputs. Its A064169 source and isolated problem contain the conjecture, without the Wolf proofs. Those grants do not establish a license for the separate results submission’s added proof code. A17.2’s license/NOTICE obligation therefore prevents transplantation on this evidence. This is a missing permission chain, not a claim that permission cannot be granted.

The submitted verification result reports Lean 4.27.0. The linked methodology pins Formal Conjectures 67338a157bbb8d87e9a349d662f82a868bda6327, whose toolchain is Lean 4.27.0 and mathlib revision is a3a10db0e9d66acbebf76c5e6a135066525ac900; the historical run’s exact mathlib pin is not established by that later methodology snapshot. The local proof uses this repository’s unchanged pins. Toolchain mismatch blocks direct dependency resolution under A17.2, but alone does not block lawful transplantation. No Wolf proof code is incorporated here.

The independently constructed local proof checks a balanced reciprocal-sum certificate in ZMod (16843^3) and then proves the structural lift to the actual natural A025529 sum. It does not claim a new discovery of the finite prime or harmonic congruence. A future admissible transplant must retire when an equivalent result is available in this repository’s own pinned mathlib, with the equivalence checked by Lean; acceptance by a future upstream alone would not establish that condition.