formal-conjectures · oeis · ams-11
Integral factorial ratio sequence:
$$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$
Supercongruence: "a(p^k) == a(p^(k-1)) ( mod p^(3*k) ) for any prime p >= 5 and any positive
integer k." - _Peter Bala_, Jan 24 2020
More generally, "the congruences a(n*p^k) == a(n*p^(k-1)) ( mod p^(3*k) ) may hold for any
prime p >= 5 and any positive integers n and k."
Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).
Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.
Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://oeis.org/A211417
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://arxiv.org/abs/2605.22763
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/OEIS/211417.lean
Local target: Corpus.OEIS211417.supercongruence
Source SHA-256: 4fa166d7d309892b255c2d686de217ba52dc3ea3dbab1eebb9751e6fdc07f018
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
Supercongruence: "a(p^k) == a(p^(k-1)) ( mod p^(3*k) ) for any prime p >= 5 and any positive integer k." - _Peter Bala_, Jan 24 2020 More generally, "the congruences a(n*p^k) == a(n*p^(k-1)) ( mod p^(3*k) ) may hold for any prime p >= 5 and any positive integers n and k."
No public records on this page.
No public records on this page.