bibkey: oeis2025a380056 authors: OEIS Foundation Inc. year: 2025 title: OEIS A380056 doi: null url: https://oeis.org/A380056 claim: A comment on OEIS A380056 conjectures that every term whose index is a multiple of four is divisible by five. strata_touched:
- D5/S3/Factorization/A380056 license: citation-only triage: anchor
OEIS A380056
The sequence is read off an exponential generating function whose numerator is the exponential minus one and whose denominator is the cosine of twice the argument. Paul D. Hanna added two conjectures on January 28, 2025; the second states that five divides every term at an index divisible by four. The caller found it still labelled Conjecture on September 9, 2026.
The two facts the page and its neighbour already supply
The same page prints a finite formula expressing an even-indexed term as a sum over binomial coefficients against Euler secant numbers and powers of four. The neighbouring entry for those Euler numbers records their periodicity modulo an odd prime, attributed to Knuth and Buckholtz in 1967; at five the period is two, so from the first index onward the residues alternate between one and zero.
Neither fact mentions the conjecture, and putting them together does not close it. Reducing the printed sum modulo five kills the terms whose Euler index is even, but what remains is a weighted binomial sum that still has to be shown to vanish. That remaining step is what the Lean module proves.
What the Lean module proves
D5/S3/Factorization/A380056 takes the two published facts as explicit
hypotheses on an abstract pair of sequences and derives the conjecture from
them. Stating it this way is deliberate: the hypotheses are the literature’s
contribution and the conclusion is not among them.
The substance is a roots-of-unity filter. The indicator of an index congruent to two modulo four is written as a combination of four powers, using that two and three have order four modulo five. The binomial theorem then collapses each power sum into a closed form, and the four closed forms cancel.
ASSUMED-UNVERIFIED: the identification of the printed sequence and formula with the module’s hypotheses is a human reading of the entry, not a machine proof that they denote the same objects. The module proves an implication; it does not verify that any particular sequence satisfies the hypotheses.
Search log
- Caller reading, 2026-09-09: the seat reported checking the entry and its full revision history, the Euler-number entry and its congruence note, and searches pairing the A-number with the divisibility claim, with the modulus, and with the generating function written out, plus a reverse search on Euler numbers modulo five which returned the classical periodicity rather than this conclusion.
- The seat’s receipt is
所查来源未找到, explicitly not a claim that no proof exists anywhere. - Caller verification, 2026-09-09: the orchestrator expanded the generating function directly and checked the conjecture, the Euler residues, the finite formula, and the vanishing of the surviving sum before dispatching a seat. Readings are in the problem entry.
Verified locator
- URL: https://oeis.org/A380056
- Euler secant numbers: https://oeis.org/A000364