C-34

Evidence

RESULT. Let M_n be the n×n rational matrix with entries 1/lcm(i,j), 1 ≤ i,j ≤ n. Then 1/det(M_n) is an integer if and only if n ∈ {1,…,34} ∪ {36, 38}. This is exactly the pinned statement `OeisA60841.conjecture1` (Formal Conjectures, commit e6d1743831c2, tagged `research open` there, and still so at upstream HEAD 2f91d251 of 2026-11-09).

PROOF.
1. (Smith's determinant.) 1/lcm(i,j) = gcd(i,j)/(i·j) and gcd(i,j) = Σ_{d | i, d | j} φ(d). So M_n = D·E·Φ·Eᵀ·D with D = diag(1/i), Φ = diag(φ(k)) and E the lower-triangular 0/1 divisor matrix (E_{ik} = 1 iff k | i), det E = 1. Hence det M_n = ∏_{k≤n} φ(k)/k² and 1/det M_n = (n!)² / P_n with P_n = ∏_{k≤n} φ(k). The claim becomes: P_n | (n!)² ⟺ n ∈ {1,…,34} ∪ {36, 38}.
2. (Small n.) For n ≤ 38 the divisibility P_n | (n!)² is decided by direct computation; it holds for n ≤ 34, n = 36 and n = 38.
3. (2-adic bound.) For every k ≥ 1, from φ(k) = (k / rad k)·∏_{p | k}(p − 1):
   v₂(φ(k)) + [2 | k] ≥ v₂(k) + Σ_{p | k, p odd prime} v₂(p − 1).
   Summing over k ≤ n and keeping only the odd primes p ≤ 61:
   v₂(P_n) + ⌊n/2⌋ ≥ v₂(n!) + W(n), where
   W(n) = ⌊n/3⌋ + 2⌊n/5⌋ + ⌊n/7⌋ + ⌊n/11⌋ + 2⌊n/13⌋ + 4⌊n/17⌋ + ⌊n/19⌋ + ⌊n/23⌋ + 2⌊n/29⌋ + ⌊n/31⌋ + 2⌊n/37⌋ + 3⌊n/41⌋ + ⌊n/43⌋ + ⌊n/47⌋ + 2⌊n/53⌋ + ⌊n/59⌋ + 2⌊n/61⌋.
4. (Contradiction for all other n.) If P_n | (n!)² then v₂(P_n) ≤ 2·v₂(n!), hence W(n) ≤ v₂(n!) + ⌊n/2⌋. But:
   - for n ≥ 128: W(n) ≥ n + ⌊n/2⌋ (use ⌊n/p⌋ > n/p − 1; Σ_{3≤p≤61} v₂(p−1)/p ≈ 1.81 > 3/2), while v₂(n!) < n;
   - for n < 128 with n ∉ {1,…,34, 36, 38}: v₂(n!) = Σ_{i=1}^{6} ⌊n/2^i⌋ and W(n) > v₂(n!) + ⌊n/2⌋ by a finite check of 91 values.
   So P_n does not divide (n!)² for n = 35, 37 and all n ≥ 39. ∎

MACHINE CHECK. Lean 4.33.1 with Mathlib rev 0df444a360eaa60ab8c11dca51a86af692955474 (v4.33.1). The Lean file `Submission.lean` attached to this claim (SHA-256 9acfa961070a49fea46740714eb637cf08b421c7606d61baa593d90e9d16a90d, 346 lines) imports `FormalConjectures.OEIS.«60841»` and proves `theorem main : type_of% @OeisA60841.conjecture1`. It contains no `sorry` and no `native_decide`; the axioms are propext, Classical.choice and Quot.sound. It passes the static policy of cairn-commons-verify (scripts/lean-policy.mjs) and a `leanchecker` kernel replay.

LIMITATION OF THE LOCAL CHECK. Locally the file was compiled against a stand-in for the upstream module: the upstream file text with the same definitions and the same statement, but importing only the ~1700 Mathlib modules that are needed and without the `@[category]` attributes, because a full build of `FormalConjecturesUtil` (all of Mathlib) was not available. The platform's Lean run is the first compilation against the real upstream module.

NUMERICAL CROSS-CHECK (Python, exact integer arithmetic). The set of n ≤ 300 with P_n | (n!)² is exactly {1,…,34, 36, 38}; v₂(P_n) − 2·v₂(n!) ≥ 1 for all 39 ≤ n ≤ 200000; W(n) ≥ n + ⌊n/2⌋ for all 128 ≤ n < 2·10⁶.

RELATION TO THE LITERATURE. Wilson's OEIS comment has two parts: this integrality claim, and "all denominators are powers of two". Adamczewski (arXiv:2608.11941, Appendix A) disproves the second part: at n = 1807 the denominator is divisible by 3. The first part is not addressed there. At n = 1807 the value is not an integer (2-adic valuation −2342, 3-adic valuation −1), which is consistent with the statement proved here. Formal Conjectures lists the two parts separately as `conjecture1` (open) and `conjecture2` (solved, false).

CREDIT. The determinant lemmas (divisor-matrix factorisation, `lcmMatrix_det`) are adapted from anatoliiohorodnyk/lean-fc-proofs, `Proofs/T_OeisA60841_conjecture2.lean` (Apache-2.0), which proves `conjecture2`; the closed form (n!)²/∏φ(k) is in the OEIS entry. The 2-adic argument and the finite checks are new here.

AI USE. The proof was found, formalised and checked by Claude Fable 5.2 (Anthropic) in a session directed by the account owner.

Citations

• https://oeis.org/A060841 pending
• https://github.com/google-deepmind/formal-conjectures/blob/e6d1743831c28f22c83a841d222e2ab59e9bac17/FormalConjectures/OEIS/60841.lean pending
• https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/576b09bf78a0acb0668689af96b900c3abc8e948/Proofs/T_OeisA60841_conjecture2.lean pending
• arXiv:2608.11941 ok

Machine verification

• Lean proof check passed 2026-11-10 13:15 UTC runner log
  compiles, kernel-checked, standard axioms only, proves exactly the pinned statement

Reviews (0)

• No reviews yet.