Kurepa's conjecture

Reference: On the left factorial function !N, by Đuro Kurepa Math. Balkanica 1, p. 147-153, 1971

def left_factorial (n : ℕ) : ℕ

Left factorial of n $$$!n = 0!+1!+2!+...+(n-1)!$$

Equations

• left_factorial n = ∑ m ∈ Finset.range n, m.factorial

theorem kurepa_conjecture (n : ℕ) (h_n : 2 < n) : left_factorial n % n ≠ 0

Kurepa's conjecture

For all $n$, $$!n\not\equiv 0 \mod n$$

This appears as B44 "Sums of factorials." in Unsolved Problems in Number Theory by Richard K. Guy

theorem kurepa_conjecture.variant.prime (p : ℕ) (h_p : 2 < p) : Nat.Prime p → left_factorial p % p ≠ 0

This statement can be reduced to the prime case only.

theorem kurepa_conjecture.prime_reduction : (∀ (n : ℕ), 2 < n → left_factorial n % n ≠ 0) ↔ ∀ (p : ℕ), 2 < p → Nat.Prime p → left_factorial p % p ≠ 0

theorem kurepa_conjecture.variant.gcd (n : ℕ) : 2 < n → n.factorial.gcd (left_factorial n) = 2

An equivalent formulation in terms of the gcd of $n!$ and $!n$.

theorem kurepa_conjecture.gcd_reduction : (∀ (n : ℕ), 2 < n → left_factorial n % n ≠ 0) ↔ ∀ (n : ℕ), 2 < n → n.factorial.gcd (left_factorial n) = 2

theorem kurepa_conjecture.variant.first_cases (n : ℕ) (h_n : 2 < n) (h_n_upper : n < 50) : left_factorial n % n ≠ 0

Sanity check: for small values we can just compute that the conjecture is true

theorem kurepa_conjecture.variant.gcd.first_cases (n : ℕ) (h_n : 2 < n) (h_n_upper : n < 50) : n.factorial.gcd (left_factorial n) = 2

Sanity check: for small values we can just compute that the conjecture is true.