FormalConjectures.Paper.Kurepa

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Kurepa's conjecture

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

namespace Kurepaopen BigOperators Nat Finset

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

def left_factorial (n : ℕ) := ∑ m ∈ Finset.range n, m !local notation "!" n => left_factorial n

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

@[category research open, AMS 11]
theorem kurepa_conjecture (n : ℕ) (h_n : 2 < n) : (!n : ℕ) % n ≠ 0 := byn:ℕh_n:2 < n⊢ (!n) % n ≠ 0
  sorryAll goals completed! 🐙

This statement can be reduced to the prime case only.

@[category research open, AMS 11]
theorem kurepa_conjecture.variants.prime (p : ℕ) (h_p : 2 < p) :
    p.Prime → (!p : ℕ) % p ≠ 0 := byp:ℕh_p:2 < p⊢ Nat.Prime p → (!p) % p ≠ 0
  sorryAll goals completed! 🐙

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


@[category textbook, AMS 11]
theorem kurepa_conjecture.prime_reduction : (∀ n, 2 < n → (!n : ℕ) % n ≠ 0)
    ↔ (∀ p, 2 < p → p.Prime → (!p : ℕ) % p ≠ 0) := by⊢ (∀ (n : ℕ), 2 < n → (!n) % n ≠ 0) ↔ ∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0
  refine ⟨fun h p hp hp_prime ↦ h p hp, fun h n hn h_mod ↦ ?_⟩h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0⊢ False
  have : n.primeFactorsList.prod ≠ n := by⊢ (∀ (n : ℕ), 2 < n → (!n) % n ≠ 0) ↔ ∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
    have (p : ℕ) (h_mem : p ∈ n.primeFactorsList) : p = 2 := by⊢ (∀ (n : ℕ), 2 < n → (!n) % n ≠ 0) ↔ ∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
      have hp : p.Prime := prime_of_mem_primeFactorsList h_memh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime p⊢ p = 2h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
      refine hp.eq_two_or_odd.resolve_right fun _ ↦ ?_h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
      have : p ∣ ∑ a ∈ range n, (a)! := .trans (byh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1⊢ p ∣ ph:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ a ∈ range n, a !⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False simpAll goals completed! 🐙h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ a ∈ range n, a !⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False)
        (dvd_of_mem_primeFactorsList h_mem |>.trans (dvd_of_mod_eq_zero h_mod))h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ a ∈ range n, a !⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
      have hxp : range p ⊆ range n := by⊢ (∀ (n : ℕ), 2 < n → (!n) % n ≠ 0) ↔ ∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ a ∈ range n, a !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
        simp only [range_subset_range]h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ a ∈ range n, a !⊢ p ≤ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ a ∈ range n, a !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
        exact le_of_mem_primeFactorsList h_memh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ a ∈ range n, a !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ a ∈ range n, a !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
      rw [← CharP.cast_eq_zero_iff (ZMod p),h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:↑(∑ a ∈ range n, a !) = 0hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False cast_sum,h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:∑ x ∈ range n, ↑x ! = 0hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
        ← sum_subset hxp (fun _ _ _ ↦ CharP.cast_eq_zero_iff _ p _ |>.2 <|
        hp.dvd_factorial.2 <| byh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝³:p % 2 = 1this:∑ x ∈ range n, ↑x ! = 0hxp:range p ⊆ range nx✝²:ℕx✝¹:x✝² ∈ range nx✝:x✝² ∉ range p⊢ p ≤ x✝²h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False aesopAll goals completed! 🐙h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False), ← cast_sum,h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:↑(∑ x ∈ range p, x !) = 0hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False CharP.cast_eq_zero_iff _ ph:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False] at thish:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
      exact h p (hp.two_le.lt_of_ne (byh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0p:ℕh_mem:p ∈ n.primeFactorsListhp:Nat.Prime px✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ 2 ≠ ph:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False omegaAll goals completed! 🐙h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False)) hp <| mod_eq_zero_of_dvd thish:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ n.primeFactorsList.prod ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
    rw [List.prod_eq_pow_card _ 2 thish:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ 2 ^ n.primeFactorsList.length ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ 2 ^ n.primeFactorsList.length ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False]h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2⊢ 2 ^ n.primeFactorsList.length ≠ nh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
    intro hh✝:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2h:2 ^ n.primeFactorsList.length = n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
    have : 4 ∣ n :=
      h ▸ pow_dvd_pow 2 ((Nat.pow_lt_pow_iff_right (n := 1) one_lt_two).1 (byh✝:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2h:2 ^ n.primeFactorsList.length = n⊢ 2 ^ 1 < 2 ^ n.primeFactorsList.lengthh✝:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this✝:∀ p ∈ n.primeFactorsList, p = 2h:2 ^ n.primeFactorsList.length = nthis:4 ∣ n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False linarithAll goals completed! 🐙h✝:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this✝:∀ p ∈ n.primeFactorsList, p = 2h:2 ^ n.primeFactorsList.length = nthis:4 ∣ n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False))h✝:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this✝:∀ p ∈ n.primeFactorsList, p = 2h:2 ^ n.primeFactorsList.length = nthis:4 ∣ n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
    have : 4 ∣ (!n : ℕ) := this.trans (dvd_of_mod_eq_zero h_mod)h✝:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this✝¹:∀ p ∈ n.primeFactorsList, p = 2h:2 ^ n.primeFactorsList.length = nthis✝:4 ∣ nthis:4 ∣ !n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
    match n with
    | S + 4 =>h✝:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕS:ℕhn:2 < S + 4h_mod:(!S + 4) % (S + 4) = 0this✝¹:∀ p ∈ (S + 4).primeFactorsList, p = 2h:2 ^ (S + 4).primeFactorsList.length = S + 4this✝:4 ∣ S + 4this:4 ∣ !S + 4⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
      simp +decide [left_factorial, mod_eq_zero_of_dvd ∘ Nat.dvd_factorial _,
        dvd_iff_mod_eq_zero,Nat.add_mod, Finset.sum_nat_mod, Finset.sum_range_succ'] at thish:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ Falseh:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:n.primeFactorsList.prod ≠ n⊢ False
  exact this <| prod_primeFactorsList hn.ne_botAll goals completed! 🐙

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

@[category research open, AMS 11]
theorem kurepa_conjecture.variants.gcd (n : ℕ) : 2 < n → (n !).gcd (! n) = 2 := byn:ℕ⊢ 2 < n → n !.gcd (!n) = 2
  sorryAll goals completed! 🐙

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.


@[category textbook, AMS 11]
theorem kurepa_conjecture.gcd_reduction : (∀ n, 2 < n → (!n : ℕ) % n ≠ 0)
    ↔ (∀ n, 2 < n → (n)!.gcd (!n) = 2) := by⊢ (∀ (n : ℕ), 2 < n → (!n) % n ≠ 0) ↔ ∀ (n : ℕ), 2 < n → n !.gcd (!n) = 2
  refine ⟨fun h n hn ↦ match n with | S + 1 => gcd_eq_iff.2 ?_,
    fun h n hn _ ↦ Nat.not_dvd_of_pos_of_lt (byh:∀ (n : ℕ), 2 < n → n !.gcd (!n) = 2n:ℕhn:2 < nx✝:(!n) % n = 0⊢ 0 < 2 omegaAll goals completed! 🐙) hn <| h n hn ▸ n.dvd_gcd
      (n.dvd_factorial hn.pos le_rfl) (dvd_of_mod_eq_zero ‹_›)⟩
  refine ⟨Nat.factorial_dvd_factorial hn.le, ?_, fun c hc h_dvd ↦ ?_⟩refine_1h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1⊢ 2 ∣ !S + 1refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1⊢ c ∣ 2
  ·refine_1h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1⊢ 2 ∣ !S + 1 match S with
    | S+1 =>h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS✝:ℕS:ℕhn:2 < S + 1 + 1⊢ 2 ∣ !S + 1 + 1 simp [mod_eq_zero_of_dvd ∘ dvd_factorial _, dvd_iff_mod_eq_zero, add_mod,
        sum_nat_mod, sum_range_succ', left_factorial]All goals completed! 🐙
  ·refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1⊢ c ∣ 2 have hc' : c ≤ S + 1 := by⊢ (∀ (n : ℕ), 2 < n → (!n) % n ≠ 0) ↔ ∀ (n : ℕ), 2 < n → n !.gcd (!n) = 2refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1hc':c ≤ S + 1⊢ c ∣ 2
      by_contrah:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1this:¬c ≤ S + 1⊢ Falserefine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1hc':c ≤ S + 1⊢ c ∣ 2
      apply h c (byh:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1this:¬c ≤ S + 1⊢ 2 < crefine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1hc':c ≤ S + 1⊢ c ∣ 2 omegaAll goals completed! 🐙refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1hc':c ≤ S + 1⊢ c ∣ 2) (c.mod_eq_zero_of_dvd ?_)
      exact (sum_range_add_sum_Ico _ (le_of_not_ge ‹_›)).subst
        (h_dvd.add (dvd_sum fun _ h => hc.trans <| Nat.factorial_dvd_factorial (byh✝:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1this:¬c ≤ S + 1x✝:ℕh:x✝ ∈ Ico (S + 1) c⊢ S + 1 ≤ x✝refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1hc':c ≤ S + 1⊢ c ∣ 2 aesopAll goals completed! 🐙refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1hc':c ≤ S + 1⊢ c ∣ 2)))refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:c ∣ !S + 1hc':c ≤ S + 1⊢ c ∣ 2
    rw [dvd_iff_mod_eq_zero,refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(!S + 1) % c = 0hc':c ≤ S + 1⊢ c ∣ 2refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ x ∈ range c, x ! % c) % c = 0hc':c ≤ S + 1⊢ c ∣ 2 left_factorial,refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ m ∈ range (S + 1), m !) % c = 0hc':c ≤ S + 1⊢ c ∣ 2refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ x ∈ range c, x ! % c) % c = 0hc':c ≤ S + 1⊢ c ∣ 2 sum_nat_mod,refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ i ∈ range (S + 1), i ! % c) % c = 0hc':c ≤ S + 1⊢ c ∣ 2refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ x ∈ range c, x ! % c) % c = 0hc':c ≤ S + 1⊢ c ∣ 2 ← sum_subset (range_mono hc')
      (byh:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ i ∈ range (S + 1), i ! % c) % c = 0hc':c ≤ S + 1⊢ ∀ x ∈ range (S + 1), x ∉ range c → x ! % c = 0refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ x ∈ range c, x ! % c) % c = 0hc':c ≤ S + 1⊢ c ∣ 2 simp +arith +contextual [mod_eq_zero_of_dvd, dvd_factorial,
        pos_of_dvd_of_pos hc (factorial_pos _)]All goals completed! 🐙refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ x ∈ range c, x ! % c) % c = 0hc':c ≤ S + 1⊢ c ∣ 2)] at h_dvdrefine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ x ∈ range c, x ! % c) % c = 0hc':c ≤ S + 1⊢ c ∣ 2
    refine by_contra fun _ ↦ h c ?_ (sum_nat_mod _ _ _ ▸ h_dvd)refine_2h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:c ∣ (S + 1)!h_dvd:(∑ x ∈ range c, x ! % c) % c = 0hc':c ≤ S + 1x✝:¬c ∣ 2⊢ 2 < c
    match c with
    | 0 =>h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:0 ∣ (S + 1)!h_dvd:(∑ x ∈ range 0, x ! % 0) % 0 = 0hc':0 ≤ S + 1x✝:¬0 ∣ 2⊢ 2 < 0
      contrapose! hch:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕh_dvd:(∑ x ∈ range 0, x ! % 0) % 0 = 0hc':0 ≤ S + 1x✝:¬0 ∣ 2hc:0 ≤ 2⊢ ¬0 ∣ (S + 1)!
      simp only [zero_dvd_iff]h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕh_dvd:(∑ x ∈ range 0, x ! % 0) % 0 = 0hc':0 ≤ S + 1x✝:¬0 ∣ 2hc:0 ≤ 2⊢ ¬(S + 1)! = 0
      positivityAll goals completed! 🐙
    | 1 =>h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS:ℕhn:2 < S + 1c:ℕhc:1 ∣ (S + 1)!h_dvd:(∑ x ∈ range 1, x ! % 1) % 1 = 0hc':1 ≤ S + 1x✝:¬1 ∣ 2⊢ 2 < 1 trivialAll goals completed! 🐙
    | S + 3 =>h:∀ (n : ℕ), 2 < n → (!n) % n ≠ 0n:ℕS✝:ℕhn:2 < S + 1c:ℕS:ℕhc:S + 3 ∣ (S✝ + 1)!h_dvd:(∑ x ∈ range (S + 3), x ! % (S + 3)) % (S + 3) = 0hc':S + 3 ≤ S✝ + 1x✝:¬S + 3 ∣ 2⊢ 2 < S + 3 omegaAll goals completed! 🐙

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

@[category test, AMS 11]
theorem kurepa_conjecture.variants.first_cases (n : ℕ) (h_n : 2 < n) (h_n_upper : n < 50) :
    (!n : ℕ) % n ≠ 0 := byn:ℕh_n:2 < nh_n_upper:n < 50⊢ (!n) % n ≠ 0
  interval_cases n«3»n:ℕh_n:2 < 3h_n_upper:3 < 50⊢ (!3) % 3 ≠ 0«4»n:ℕh_n:2 < 4h_n_upper:4 < 50⊢ (!4) % 4 ≠ 0«5»n:ℕh_n:2 < 5h_n_upper:5 < 50⊢ (!5) % 5 ≠ 0«6»n:ℕh_n:2 < 6h_n_upper:6 < 50⊢ (!6) % 6 ≠ 0«7»n:ℕh_n:2 < 7h_n_upper:7 < 50⊢ (!7) % 7 ≠ 0«8»n:ℕh_n:2 < 8h_n_upper:8 < 50⊢ (!8) % 8 ≠ 0«9»n:ℕh_n:2 < 9h_n_upper:9 < 50⊢ (!9) % 9 ≠ 0«10»n:ℕh_n:2 < 10h_n_upper:10 < 50⊢ (!10) % 10 ≠ 0«11»n:ℕh_n:2 < 11h_n_upper:11 < 50⊢ (!11) % 11 ≠ 0«12»n:ℕh_n:2 < 12h_n_upper:12 < 50⊢ (!12) % 12 ≠ 0«13»n:ℕh_n:2 < 13h_n_upper:13 < 50⊢ (!13) % 13 ≠ 0«14»n:ℕh_n:2 < 14h_n_upper:14 < 50⊢ (!14) % 14 ≠ 0«15»n:ℕh_n:2 < 15h_n_upper:15 < 50⊢ (!15) % 15 ≠ 0«16»n:ℕh_n:2 < 16h_n_upper:16 < 50⊢ (!16) % 16 ≠ 0«17»n:ℕh_n:2 < 17h_n_upper:17 < 50⊢ (!17) % 17 ≠ 0«18»n:ℕh_n:2 < 18h_n_upper:18 < 50⊢ (!18) % 18 ≠ 0«19»n:ℕh_n:2 < 19h_n_upper:19 < 50⊢ (!19) % 19 ≠ 0«20»n:ℕh_n:2 < 20h_n_upper:20 < 50⊢ (!20) % 20 ≠ 0«21»n:ℕh_n:2 < 21h_n_upper:21 < 50⊢ (!21) % 21 ≠ 0«22»n:ℕh_n:2 < 22h_n_upper:22 < 50⊢ (!22) % 22 ≠ 0«23»n:ℕh_n:2 < 23h_n_upper:23 < 50⊢ (!23) % 23 ≠ 0«24»n:ℕh_n:2 < 24h_n_upper:24 < 50⊢ (!24) % 24 ≠ 0«25»n:ℕh_n:2 < 25h_n_upper:25 < 50⊢ (!25) % 25 ≠ 0«26»n:ℕh_n:2 < 26h_n_upper:26 < 50⊢ (!26) % 26 ≠ 0«27»n:ℕh_n:2 < 27h_n_upper:27 < 50⊢ (!27) % 27 ≠ 0«28»n:ℕh_n:2 < 28h_n_upper:28 < 50⊢ (!28) % 28 ≠ 0«29»n:ℕh_n:2 < 29h_n_upper:29 < 50⊢ (!29) % 29 ≠ 0«30»n:ℕh_n:2 < 30h_n_upper:30 < 50⊢ (!30) % 30 ≠ 0«31»n:ℕh_n:2 < 31h_n_upper:31 < 50⊢ (!31) % 31 ≠ 0«32»n:ℕh_n:2 < 32h_n_upper:32 < 50⊢ (!32) % 32 ≠ 0«33»n:ℕh_n:2 < 33h_n_upper:33 < 50⊢ (!33) % 33 ≠ 0«34»n:ℕh_n:2 < 34h_n_upper:34 < 50⊢ (!34) % 34 ≠ 0«35»n:ℕh_n:2 < 35h_n_upper:35 < 50⊢ (!35) % 35 ≠ 0«36»n:ℕh_n:2 < 36h_n_upper:36 < 50⊢ (!36) % 36 ≠ 0«37»n:ℕh_n:2 < 37h_n_upper:37 < 50⊢ (!37) % 37 ≠ 0«38»n:ℕh_n:2 < 38h_n_upper:38 < 50⊢ (!38) % 38 ≠ 0«39»n:ℕh_n:2 < 39h_n_upper:39 < 50⊢ (!39) % 39 ≠ 0«40»n:ℕh_n:2 < 40h_n_upper:40 < 50⊢ (!40) % 40 ≠ 0«41»n:ℕh_n:2 < 41h_n_upper:41 < 50⊢ (!41) % 41 ≠ 0«42»n:ℕh_n:2 < 42h_n_upper:42 < 50⊢ (!42) % 42 ≠ 0«43»n:ℕh_n:2 < 43h_n_upper:43 < 50⊢ (!43) % 43 ≠ 0«44»n:ℕh_n:2 < 44h_n_upper:44 < 50⊢ (!44) % 44 ≠ 0«45»n:ℕh_n:2 < 45h_n_upper:45 < 50⊢ (!45) % 45 ≠ 0«46»n:ℕh_n:2 < 46h_n_upper:46 < 50⊢ (!46) % 46 ≠ 0«47»n:ℕh_n:2 < 47h_n_upper:47 < 50⊢ (!47) % 47 ≠ 0«48»n:ℕh_n:2 < 48h_n_upper:48 < 50⊢ (!48) % 48 ≠ 0«49»n:ℕh_n:2 < 49h_n_upper:49 < 50⊢ (!49) % 49 ≠ 0 <;>«3»n:ℕh_n:2 < 3h_n_upper:3 < 50⊢ (!3) % 3 ≠ 0«4»n:ℕh_n:2 < 4h_n_upper:4 < 50⊢ (!4) % 4 ≠ 0«5»n:ℕh_n:2 < 5h_n_upper:5 < 50⊢ (!5) % 5 ≠ 0«6»n:ℕh_n:2 < 6h_n_upper:6 < 50⊢ (!6) % 6 ≠ 0«7»n:ℕh_n:2 < 7h_n_upper:7 < 50⊢ (!7) % 7 ≠ 0«8»n:ℕh_n:2 < 8h_n_upper:8 < 50⊢ (!8) % 8 ≠ 0«9»n:ℕh_n:2 < 9h_n_upper:9 < 50⊢ (!9) % 9 ≠ 0«10»n:ℕh_n:2 < 10h_n_upper:10 < 50⊢ (!10) % 10 ≠ 0«11»n:ℕh_n:2 < 11h_n_upper:11 < 50⊢ (!11) % 11 ≠ 0«12»n:ℕh_n:2 < 12h_n_upper:12 < 50⊢ (!12) % 12 ≠ 0«13»n:ℕh_n:2 < 13h_n_upper:13 < 50⊢ (!13) % 13 ≠ 0«14»n:ℕh_n:2 < 14h_n_upper:14 < 50⊢ (!14) % 14 ≠ 0«15»n:ℕh_n:2 < 15h_n_upper:15 < 50⊢ (!15) % 15 ≠ 0«16»n:ℕh_n:2 < 16h_n_upper:16 < 50⊢ (!16) % 16 ≠ 0«17»n:ℕh_n:2 < 17h_n_upper:17 < 50⊢ (!17) % 17 ≠ 0«18»n:ℕh_n:2 < 18h_n_upper:18 < 50⊢ (!18) % 18 ≠ 0«19»n:ℕh_n:2 < 19h_n_upper:19 < 50⊢ (!19) % 19 ≠ 0«20»n:ℕh_n:2 < 20h_n_upper:20 < 50⊢ (!20) % 20 ≠ 0«21»n:ℕh_n:2 < 21h_n_upper:21 < 50⊢ (!21) % 21 ≠ 0«22»n:ℕh_n:2 < 22h_n_upper:22 < 50⊢ (!22) % 22 ≠ 0«23»n:ℕh_n:2 < 23h_n_upper:23 < 50⊢ (!23) % 23 ≠ 0«24»n:ℕh_n:2 < 24h_n_upper:24 < 50⊢ (!24) % 24 ≠ 0«25»n:ℕh_n:2 < 25h_n_upper:25 < 50⊢ (!25) % 25 ≠ 0«26»n:ℕh_n:2 < 26h_n_upper:26 < 50⊢ (!26) % 26 ≠ 0«27»n:ℕh_n:2 < 27h_n_upper:27 < 50⊢ (!27) % 27 ≠ 0«28»n:ℕh_n:2 < 28h_n_upper:28 < 50⊢ (!28) % 28 ≠ 0«29»n:ℕh_n:2 < 29h_n_upper:29 < 50⊢ (!29) % 29 ≠ 0«30»n:ℕh_n:2 < 30h_n_upper:30 < 50⊢ (!30) % 30 ≠ 0«31»n:ℕh_n:2 < 31h_n_upper:31 < 50⊢ (!31) % 31 ≠ 0«32»n:ℕh_n:2 < 32h_n_upper:32 < 50⊢ (!32) % 32 ≠ 0«33»n:ℕh_n:2 < 33h_n_upper:33 < 50⊢ (!33) % 33 ≠ 0«34»n:ℕh_n:2 < 34h_n_upper:34 < 50⊢ (!34) % 34 ≠ 0«35»n:ℕh_n:2 < 35h_n_upper:35 < 50⊢ (!35) % 35 ≠ 0«36»n:ℕh_n:2 < 36h_n_upper:36 < 50⊢ (!36) % 36 ≠ 0«37»n:ℕh_n:2 < 37h_n_upper:37 < 50⊢ (!37) % 37 ≠ 0«38»n:ℕh_n:2 < 38h_n_upper:38 < 50⊢ (!38) % 38 ≠ 0«39»n:ℕh_n:2 < 39h_n_upper:39 < 50⊢ (!39) % 39 ≠ 0«40»n:ℕh_n:2 < 40h_n_upper:40 < 50⊢ (!40) % 40 ≠ 0«41»n:ℕh_n:2 < 41h_n_upper:41 < 50⊢ (!41) % 41 ≠ 0«42»n:ℕh_n:2 < 42h_n_upper:42 < 50⊢ (!42) % 42 ≠ 0«43»n:ℕh_n:2 < 43h_n_upper:43 < 50⊢ (!43) % 43 ≠ 0«44»n:ℕh_n:2 < 44h_n_upper:44 < 50⊢ (!44) % 44 ≠ 0«45»n:ℕh_n:2 < 45h_n_upper:45 < 50⊢ (!45) % 45 ≠ 0«46»n:ℕh_n:2 < 46h_n_upper:46 < 50⊢ (!46) % 46 ≠ 0«47»n:ℕh_n:2 < 47h_n_upper:47 < 50⊢ (!47) % 47 ≠ 0«48»n:ℕh_n:2 < 48h_n_upper:48 < 50⊢ (!48) % 48 ≠ 0«49»n:ℕh_n:2 < 49h_n_upper:49 < 50⊢ (!49) % 49 ≠ 0 decideAll goals completed! 🐙

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

@[category test, AMS 11]
theorem kurepa_conjecture.variants.gcd.first_cases (n : ℕ) (h_n : 2 < n) (h_n_upper : n < 50) :
    (n !).gcd (! n) = 2 := byn:ℕh_n:2 < nh_n_upper:n < 50⊢ n !.gcd (!n) = 2
  interval_cases n«3»n:ℕh_n:2 < 3h_n_upper:3 < 50⊢ 3!.gcd (!3) = 2«4»n:ℕh_n:2 < 4h_n_upper:4 < 50⊢ 4!.gcd (!4) = 2«5»n:ℕh_n:2 < 5h_n_upper:5 < 50⊢ 5!.gcd (!5) = 2«6»n:ℕh_n:2 < 6h_n_upper:6 < 50⊢ 6!.gcd (!6) = 2«7»n:ℕh_n:2 < 7h_n_upper:7 < 50⊢ 7!.gcd (!7) = 2«8»n:ℕh_n:2 < 8h_n_upper:8 < 50⊢ 8!.gcd (!8) = 2«9»n:ℕh_n:2 < 9h_n_upper:9 < 50⊢ 9!.gcd (!9) = 2«10»n:ℕh_n:2 < 10h_n_upper:10 < 50⊢ 10!.gcd (!10) = 2«11»n:ℕh_n:2 < 11h_n_upper:11 < 50⊢ 11!.gcd (!11) = 2«12»n:ℕh_n:2 < 12h_n_upper:12 < 50⊢ 12!.gcd (!12) = 2«13»n:ℕh_n:2 < 13h_n_upper:13 < 50⊢ 13!.gcd (!13) = 2«14»n:ℕh_n:2 < 14h_n_upper:14 < 50⊢ 14!.gcd (!14) = 2«15»n:ℕh_n:2 < 15h_n_upper:15 < 50⊢ 15!.gcd (!15) = 2«16»n:ℕh_n:2 < 16h_n_upper:16 < 50⊢ 16!.gcd (!16) = 2«17»n:ℕh_n:2 < 17h_n_upper:17 < 50⊢ 17!.gcd (!17) = 2«18»n:ℕh_n:2 < 18h_n_upper:18 < 50⊢ 18!.gcd (!18) = 2«19»n:ℕh_n:2 < 19h_n_upper:19 < 50⊢ 19!.gcd (!19) = 2«20»n:ℕh_n:2 < 20h_n_upper:20 < 50⊢ 20!.gcd (!20) = 2«21»n:ℕh_n:2 < 21h_n_upper:21 < 50⊢ 21!.gcd (!21) = 2«22»n:ℕh_n:2 < 22h_n_upper:22 < 50⊢ 22!.gcd (!22) = 2«23»n:ℕh_n:2 < 23h_n_upper:23 < 50⊢ 23!.gcd (!23) = 2«24»n:ℕh_n:2 < 24h_n_upper:24 < 50⊢ 24!.gcd (!24) = 2«25»n:ℕh_n:2 < 25h_n_upper:25 < 50⊢ 25!.gcd (!25) = 2«26»n:ℕh_n:2 < 26h_n_upper:26 < 50⊢ 26!.gcd (!26) = 2«27»n:ℕh_n:2 < 27h_n_upper:27 < 50⊢ 27!.gcd (!27) = 2«28»n:ℕh_n:2 < 28h_n_upper:28 < 50⊢ 28!.gcd (!28) = 2«29»n:ℕh_n:2 < 29h_n_upper:29 < 50⊢ 29!.gcd (!29) = 2«30»n:ℕh_n:2 < 30h_n_upper:30 < 50⊢ 30!.gcd (!30) = 2«31»n:ℕh_n:2 < 31h_n_upper:31 < 50⊢ 31!.gcd (!31) = 2«32»n:ℕh_n:2 < 32h_n_upper:32 < 50⊢ 32!.gcd (!32) = 2«33»n:ℕh_n:2 < 33h_n_upper:33 < 50⊢ 33!.gcd (!33) = 2«34»n:ℕh_n:2 < 34h_n_upper:34 < 50⊢ 34!.gcd (!34) = 2«35»n:ℕh_n:2 < 35h_n_upper:35 < 50⊢ 35!.gcd (!35) = 2«36»n:ℕh_n:2 < 36h_n_upper:36 < 50⊢ 36!.gcd (!36) = 2«37»n:ℕh_n:2 < 37h_n_upper:37 < 50⊢ 37!.gcd (!37) = 2«38»n:ℕh_n:2 < 38h_n_upper:38 < 50⊢ 38!.gcd (!38) = 2«39»n:ℕh_n:2 < 39h_n_upper:39 < 50⊢ 39!.gcd (!39) = 2«40»n:ℕh_n:2 < 40h_n_upper:40 < 50⊢ 40!.gcd (!40) = 2«41»n:ℕh_n:2 < 41h_n_upper:41 < 50⊢ 41!.gcd (!41) = 2«42»n:ℕh_n:2 < 42h_n_upper:42 < 50⊢ 42!.gcd (!42) = 2«43»n:ℕh_n:2 < 43h_n_upper:43 < 50⊢ 43!.gcd (!43) = 2«44»n:ℕh_n:2 < 44h_n_upper:44 < 50⊢ 44!.gcd (!44) = 2«45»n:ℕh_n:2 < 45h_n_upper:45 < 50⊢ 45!.gcd (!45) = 2«46»n:ℕh_n:2 < 46h_n_upper:46 < 50⊢ 46!.gcd (!46) = 2«47»n:ℕh_n:2 < 47h_n_upper:47 < 50⊢ 47!.gcd (!47) = 2«48»n:ℕh_n:2 < 48h_n_upper:48 < 50⊢ 48!.gcd (!48) = 2«49»n:ℕh_n:2 < 49h_n_upper:49 < 50⊢ 49!.gcd (!49) = 2 <;>«3»n:ℕh_n:2 < 3h_n_upper:3 < 50⊢ 3!.gcd (!3) = 2«4»n:ℕh_n:2 < 4h_n_upper:4 < 50⊢ 4!.gcd (!4) = 2«5»n:ℕh_n:2 < 5h_n_upper:5 < 50⊢ 5!.gcd (!5) = 2«6»n:ℕh_n:2 < 6h_n_upper:6 < 50⊢ 6!.gcd (!6) = 2«7»n:ℕh_n:2 < 7h_n_upper:7 < 50⊢ 7!.gcd (!7) = 2«8»n:ℕh_n:2 < 8h_n_upper:8 < 50⊢ 8!.gcd (!8) = 2«9»n:ℕh_n:2 < 9h_n_upper:9 < 50⊢ 9!.gcd (!9) = 2«10»n:ℕh_n:2 < 10h_n_upper:10 < 50⊢ 10!.gcd (!10) = 2«11»n:ℕh_n:2 < 11h_n_upper:11 < 50⊢ 11!.gcd (!11) = 2«12»n:ℕh_n:2 < 12h_n_upper:12 < 50⊢ 12!.gcd (!12) = 2«13»n:ℕh_n:2 < 13h_n_upper:13 < 50⊢ 13!.gcd (!13) = 2«14»n:ℕh_n:2 < 14h_n_upper:14 < 50⊢ 14!.gcd (!14) = 2«15»n:ℕh_n:2 < 15h_n_upper:15 < 50⊢ 15!.gcd (!15) = 2«16»n:ℕh_n:2 < 16h_n_upper:16 < 50⊢ 16!.gcd (!16) = 2«17»n:ℕh_n:2 < 17h_n_upper:17 < 50⊢ 17!.gcd (!17) = 2«18»n:ℕh_n:2 < 18h_n_upper:18 < 50⊢ 18!.gcd (!18) = 2«19»n:ℕh_n:2 < 19h_n_upper:19 < 50⊢ 19!.gcd (!19) = 2«20»n:ℕh_n:2 < 20h_n_upper:20 < 50⊢ 20!.gcd (!20) = 2«21»n:ℕh_n:2 < 21h_n_upper:21 < 50⊢ 21!.gcd (!21) = 2«22»n:ℕh_n:2 < 22h_n_upper:22 < 50⊢ 22!.gcd (!22) = 2«23»n:ℕh_n:2 < 23h_n_upper:23 < 50⊢ 23!.gcd (!23) = 2«24»n:ℕh_n:2 < 24h_n_upper:24 < 50⊢ 24!.gcd (!24) = 2«25»n:ℕh_n:2 < 25h_n_upper:25 < 50⊢ 25!.gcd (!25) = 2«26»n:ℕh_n:2 < 26h_n_upper:26 < 50⊢ 26!.gcd (!26) = 2«27»n:ℕh_n:2 < 27h_n_upper:27 < 50⊢ 27!.gcd (!27) = 2«28»n:ℕh_n:2 < 28h_n_upper:28 < 50⊢ 28!.gcd (!28) = 2«29»n:ℕh_n:2 < 29h_n_upper:29 < 50⊢ 29!.gcd (!29) = 2«30»n:ℕh_n:2 < 30h_n_upper:30 < 50⊢ 30!.gcd (!30) = 2«31»n:ℕh_n:2 < 31h_n_upper:31 < 50⊢ 31!.gcd (!31) = 2«32»n:ℕh_n:2 < 32h_n_upper:32 < 50⊢ 32!.gcd (!32) = 2«33»n:ℕh_n:2 < 33h_n_upper:33 < 50⊢ 33!.gcd (!33) = 2«34»n:ℕh_n:2 < 34h_n_upper:34 < 50⊢ 34!.gcd (!34) = 2«35»n:ℕh_n:2 < 35h_n_upper:35 < 50⊢ 35!.gcd (!35) = 2«36»n:ℕh_n:2 < 36h_n_upper:36 < 50⊢ 36!.gcd (!36) = 2«37»n:ℕh_n:2 < 37h_n_upper:37 < 50⊢ 37!.gcd (!37) = 2«38»n:ℕh_n:2 < 38h_n_upper:38 < 50⊢ 38!.gcd (!38) = 2«39»n:ℕh_n:2 < 39h_n_upper:39 < 50⊢ 39!.gcd (!39) = 2«40»n:ℕh_n:2 < 40h_n_upper:40 < 50⊢ 40!.gcd (!40) = 2«41»n:ℕh_n:2 < 41h_n_upper:41 < 50⊢ 41!.gcd (!41) = 2«42»n:ℕh_n:2 < 42h_n_upper:42 < 50⊢ 42!.gcd (!42) = 2«43»n:ℕh_n:2 < 43h_n_upper:43 < 50⊢ 43!.gcd (!43) = 2«44»n:ℕh_n:2 < 44h_n_upper:44 < 50⊢ 44!.gcd (!44) = 2«45»n:ℕh_n:2 < 45h_n_upper:45 < 50⊢ 45!.gcd (!45) = 2«46»n:ℕh_n:2 < 46h_n_upper:46 < 50⊢ 46!.gcd (!46) = 2«47»n:ℕh_n:2 < 47h_n_upper:47 < 50⊢ 47!.gcd (!47) = 2«48»n:ℕh_n:2 < 48h_n_upper:48 < 50⊢ 48!.gcd (!48) = 2«49»n:ℕh_n:2 < 49h_n_upper:49 < 50⊢ 49!.gcd (!49) = 2 decideAll goals completed! 🐙

end Kurepa