Central factorial numbers: $((2n)!!)^2$

formal-conjectures · oeis · ams-11 · ams-15

Central factorial numbers: $a(n) = 4^n (n!)^2 = ((2n)!!)^2$.

Let $\zeta$ be a primitive $(2n+1)$-th root of unity. Then the permanent of the
$2n \times 2n$ matrix $[m(j,k)]_{j,k=1..2n}$ is $a(n)/(2n+1) = ((2n)!!)^2/(2n+1)$,
where $m(j,k)$ is $1$ or $(1+\zeta^{j-k})/(1-\zeta^{j-k})$ according as $j = k$ or not.
- Zhi-Wei Sun, Dec 21 2021

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/A002454
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/OEIS/2454.lean
Local target: Corpus.OEIS2454.conjecture
Source SHA-256: d9c478c382e9489c22d89374838e8a3f39b9a443b23933910108eb43011af501
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.

Public JSON record