Kurepa's conjecture

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

def Kurepa.left_factorial (n : ℕ) : ℕ

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

Equations

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

theorem Kurepa.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.kurepa_conjecture.variants.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.kurepa_conjecture.prime_reduction : (∀ (n : ℕ), 2 < n → left_factorial n % n ≠ 0) ↔ ∀ (p : ℕ), 2 < p → Nat.Prime p → left_factorial p % p ≠ 0

Kurepa's conjecture for all integers greater than 2 is equivalent to the conjecture restricted to primes greater than 2.

theorem Kurepa.kurepa_conjecture.variants.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.kurepa_conjecture.gcd_reduction : (∀ (n : ℕ), 2 < n → left_factorial n % n ≠ 0) ↔ ∀ (n : ℕ), 2 < n → n.factorial.gcd (left_factorial n) = 2

Kurepa's conjecture for all integers greater than 2 is equivalent to the statement that $\gcd(n!, !n) = 2$ for all integers greater than 2.

theorem Kurepa.kurepa_conjecture.variants.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.kurepa_conjecture.variants.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.