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 Kurepa


open 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 declaration uses 'sorry'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 declaration uses 'sorry'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 ≠ 0
    have (p : ℕ) (h_mem : p ∈ n.primeFactorsList) : p = 2 := by⊢ (∀ (n : ℕ), 2 < n → (!n) % n ≠ 0) ↔ ∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0
      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 := prime_of_mem_primeFactorsList h_mem⊢ p = 2
      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 p := prime_of_mem_primeFactorsList h_memx✝:p % 2 = 1⊢ 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 p := prime_of_mem_primeFactorsList h_memx✝:p % 2 = 1⊢ p ∣ p simpAll goals completed! 🐙)
        (dvd_of_mem_primeFactorsList h_mem |>.trans (dvd_of_mod_eq_zero h_mod))
      have hxp : range p ⊆ range n := by⊢ (∀ (n : ℕ), 2 < n → (!n) % n ≠ 0) ↔ ∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0
        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 p := prime_of_mem_primeFactorsList h_memx✝:p % 2 = 1this:p ∣ ∑ a ∈ range n, a ! := 
  Dvd.dvd.trans (of_eq_true (dvd_refl._simp_1 p))
    (Dvd.dvd.trans (dvd_of_mem_primeFactorsList h_mem) (dvd_of_mod_eq_zero h_mod))⊢ p ≤ n
        exact le_of_mem_primeFactorsList h_memAll goals completed! 🐙
      rw [← CharP.cast_eq_zero_iff (ZMod p), cast_sum,
        ← sum_subset hxp (fun _ _ _ ↦ CharP.cast_eq_zero_iff _ p _ |>.2 <|
        hp.dvd_factorial.2 <| by aesop), ← cast_sum, CharP.cast_eq_zero_iff _ p] 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 p := prime_of_mem_primeFactorsList h_memx✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range 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 p := prime_of_mem_primeFactorsList h_memx✝:p % 2 = 1this:p ∣ ∑ x ∈ range p, x !hxp:range p ⊆ range n⊢ 2 ≠ p omegaAll goals completed! 🐙)) hp <| mod_eq_zero_of_dvd this
    rw [List.prod_eq_pow_card _ 2 this]h:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2 := 
  fun p h_mem =>
    have hp := prime_of_mem_primeFactorsList h_mem;
    Or.resolve_right (Prime.eq_two_or_odd hp) fun x =>
      have this :=
        Dvd.dvd.trans (of_eq_true (dvd_refl._simp_1 p))
          (Dvd.dvd.trans (dvd_of_mem_primeFactorsList h_mem) (dvd_of_mod_eq_zero h_mod));
      have hxp := Eq.mpr (id prime_reduction._simp_1) (le_of_mem_primeFactorsList h_mem);
      h p (LE.le.lt_of_ne (Prime.two_le hp) fun a => prime_reduction._proof_2 n p x a) hp
        (mod_eq_zero_of_dvd
          (Eq.mp (congrArg (fun _a => _a) (propext (CharP.cast_eq_zero_iff (ZMod p) p (∑ x ∈ range p, x !))))
            (Eq.mp (congrArg (fun _a => _a = 0) (Eq.symm (cast_sum (range p) factorial)))
              (Eq.mp
                (congrArg (fun _a => _a = 0)
                  (Eq.symm
                    (sum_subset hxp fun x x_1 x_2 =>
                      (CharP.cast_eq_zero_iff (ZMod p) p x !).mpr
                        ((Prime.dvd_factorial hp).mpr
                          (id (Eq.mp (Eq.trans (congrArg Not mem_range._simp_1) not_lt._simp_1) x_2))))))
                (Eq.mp (congrArg (fun _a => _a = 0) (cast_sum (range n) factorial))
                  (Eq.mp
                    (congrArg (fun _a => _a) (Eq.symm (propext (CharP.cast_eq_zero_iff (ZMod p) p (∑ a ∈ range n, a !)))))
                    this))))))⊢ 2 ^ n.primeFactorsList.length ≠ n
    intro hh✝:∀ (p : ℕ), 2 < p → Nat.Prime p → (!p) % p ≠ 0n:ℕhn:2 < nh_mod:(!n) % n = 0this:∀ p ∈ n.primeFactorsList, p = 2 := 
  fun p h_mem =>
    have hp := prime_of_mem_primeFactorsList h_mem;
    Or.resolve_right (Prime.eq_two_or_odd hp) fun x =>
      have this :=
        Dvd.dvd.trans (of_eq_true (dvd_refl._simp_1 p))
          (Dvd.dvd.trans (dvd_of_mem_primeFactorsList h_mem) (dvd_of_mod_eq_zero h_mod));
      have hxp := Eq.mpr (id prime_reduction._simp_1) (le_of_mem_primeFactorsList h_mem);
      h p (LE.le.lt_of_ne (Prime.two_le hp) fun a => prime_reduction._proof_2 n p x a) hp
        (mod_eq_zero_of_dvd
          (Eq.mp (congrArg (fun _a => _a) (propext (CharP.cast_eq_zero_iff (ZMod p) p (∑ x ∈ range p, x !))))
            (Eq.mp (congrArg (fun _a => _a = 0) (Eq.symm (cast_sum (range p) factorial)))
              (Eq.mp
                (congrArg (fun _a => _a = 0)
                  (Eq.symm
                    (sum_subset hxp fun x x_1 x_2 =>
                      (CharP.cast_eq_zero_iff (ZMod p) p x !).mpr
                        ((Prime.dvd_factorial hp).mpr
                          (id (Eq.mp (Eq.trans (congrArg Not mem_range._simp_1) not_lt._simp_1) x_2))))))
                (Eq.mp (congrArg (fun _a => _a = 0) (cast_sum (range n) factorial))
                  (Eq.mp
                    (congrArg (fun _a => _a) (Eq.symm (propext (CharP.cast_eq_zero_iff (ZMod p) p (∑ a ∈ range n, a !)))))
                    this))))))h:2 ^ n.primeFactorsList.length = 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 = 2 := 
  fun p h_mem =>
    have hp := prime_of_mem_primeFactorsList h_mem;
    Or.resolve_right (Prime.eq_two_or_odd hp) fun x =>
      have this :=
        Dvd.dvd.trans (of_eq_true (dvd_refl._simp_1 p))
          (Dvd.dvd.trans (dvd_of_mem_primeFactorsList h_mem) (dvd_of_mod_eq_zero h_mod));
      have hxp := Eq.mpr (id prime_reduction._simp_1) (le_of_mem_primeFactorsList h_mem);
      h✝ p (LE.le.lt_of_ne (Prime.two_le hp) fun a => prime_reduction._proof_2 n p x a) hp
        (mod_eq_zero_of_dvd
          (Eq.mp (congrArg (fun _a => _a) (propext (CharP.cast_eq_zero_iff (ZMod p) p (∑ x ∈ range p, x !))))
            (Eq.mp (congrArg (fun _a => _a = 0) (Eq.symm (cast_sum (range p) factorial)))
              (Eq.mp
                (congrArg (fun _a => _a = 0)
                  (Eq.symm
                    (sum_subset hxp fun x x_1 x_2 =>
                      (CharP.cast_eq_zero_iff (ZMod p) p x !).mpr
                        ((Prime.dvd_factorial hp).mpr
                          (id (Eq.mp (Eq.trans (congrArg Not mem_range._simp_1) not_lt._simp_1) x_2))))))
                (Eq.mp (congrArg (fun _a => _a = 0) (cast_sum (range n) factorial))
                  (Eq.mp
                    (congrArg (fun _a => _a) (Eq.symm (propext (CharP.cast_eq_zero_iff (ZMod p) p (∑ a ∈ range n, a !)))))
                    this))))))h:2 ^ n.primeFactorsList.length = n⊢ 2 ^ 1 < 2 ^ n.primeFactorsList.length linarithAll goals completed! 🐙))
    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 = 2 := 
  fun p h_mem =>
    have hp := prime_of_mem_primeFactorsList h_mem;
    Or.resolve_right (Prime.eq_two_or_odd hp) fun x =>
      have this :=
        Dvd.dvd.trans (of_eq_true (dvd_refl._simp_1 p))
          (Dvd.dvd.trans (dvd_of_mem_primeFactorsList h_mem) (dvd_of_mod_eq_zero h_mod));
      have hxp := Eq.mpr (id prime_reduction._simp_1) (le_of_mem_primeFactorsList h_mem);
      h p (LE.le.lt_of_ne (Prime.two_le hp) fun a => prime_reduction._proof_2 n p x a) hp
        (mod_eq_zero_of_dvd
          (Eq.mp (congrArg (fun _a => _a) (propext (CharP.cast_eq_zero_iff (ZMod p) p (∑ x ∈ range p, x !))))
            (Eq.mp (congrArg (fun _a => _a = 0) (Eq.symm (cast_sum (range p) factorial)))
              (Eq.mp
                (congrArg (fun _a => _a = 0)
                  (Eq.symm
                    (sum_subset hxp fun x x_1 x_2 =>
                      (CharP.cast_eq_zero_iff (ZMod p) p x !).mpr
                        ((Prime.dvd_factorial hp).mpr
                          (id (Eq.mp (Eq.trans (congrArg Not mem_range._simp_1) not_lt._simp_1) x_2))))))
                (Eq.mp (congrArg (fun _a => _a = 0) (cast_sum (range n) factorial))
                  (Eq.mp
                    (congrArg (fun _a => _a) (Eq.symm (propext (CharP.cast_eq_zero_iff (ZMod p) p (∑ a ∈ range n, a !)))))
                    this))))))h:2 ^ n.primeFactorsList.length = nthis✝:4 ∣ n := 
  h ▸
    pow_dvd_pow 2
      ((Nat.pow_lt_pow_iff_right one_lt_two).mp
        (lt_of_not_ge fun a =>
          Mathlib.Tactic.Linarith.lt_irrefl
            (Eq.mp
              (congrArg (fun _a => _a < 0)
                (Mathlib.Tactic.Ring.of_eq
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.add_congr
                      (Mathlib.Tactic.Ring.add_congr
                        (Mathlib.Tactic.Ring.neg_congr
                          (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                          (Mathlib.Tactic.Ring.neg_add
                            (Mathlib.Tactic.Ring.neg_one_mul
                              (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                  (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                                  (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                                  (Eq.refl (Int.negOfNat 1)))))
                            Mathlib.Tactic.Ring.neg_zero))
                        (Mathlib.Tactic.Ring.sub_congr
                          (Mathlib.Tactic.Ring.add_congr
                            (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                            (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                            (Mathlib.Tactic.Ring.add_pf_add_overlap
                              (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                                (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd)
                                  (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                                  (Eq.refl 3)))
                              (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                          (Mathlib.Tactic.Ring.atom_pf ↑n)
                          (Mathlib.Tactic.Ring.sub_pf
                            (Mathlib.Tactic.Ring.neg_add
                              (Mathlib.Tactic.Ring.neg_mul (↑n) (rawCast 1)
                                (Mathlib.Tactic.Ring.neg_one_mul
                                  (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                    (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                                      (Eq.refl (Int.negOfNat 1))))))
                              Mathlib.Tactic.Ring.neg_zero)
                            (Mathlib.Tactic.Ring.add_pf_add_lt (rawCast 3)
                              (Mathlib.Tactic.Ring.add_pf_zero_add (↑n ^ rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                        (Mathlib.Tactic.Ring.add_pf_add_overlap
                          (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                            (Mathlib.Meta.NormNum.IsInt.to_isNat
                              (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                                (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 3))
                                (Eq.refl (Int.ofNat 2)))))
                          (Mathlib.Tactic.Ring.add_pf_zero_add (↑n ^ rawCast 1 * (Int.negOfNat 1).rawCast + 0))))
                      (Mathlib.Tactic.Ring.neg_congr
                        (Mathlib.Tactic.Ring.sub_congr
                          (Mathlib.Tactic.Ring.pow_congr
                            (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                            (Mathlib.Tactic.Ring.atom_pf n.primeFactorsList.length)
                            (Mathlib.Tactic.Ring.pow_add
                              (Mathlib.Tactic.Ring.single_pow
                                (Mathlib.Tactic.Ring.pow_prod_atom (rawCast 2)
                                  (n.primeFactorsList.length ^ rawCast 1 * rawCast 1)))
                              (Mathlib.Tactic.Ring.pow_zero (rawCast 2 + 0))
                              (Mathlib.Tactic.Ring.add_mul
                                (Mathlib.Tactic.Ring.mul_add
                                  (Mathlib.Tactic.Ring.mul_pf_left (rawCast 2 + 0)
                                    (n.primeFactorsList.length ^ rawCast 1 * rawCast 1)
                                    (Mathlib.Tactic.Ring.one_mul (rawCast 1)))
                                  (Mathlib.Tactic.Ring.mul_zero
                                    ((rawCast 2 + 0) ^ (n.primeFactorsList.length ^ rawCast 1 * rawCast 1) * rawCast 1))
                                  (Mathlib.Tactic.Ring.add_pf_add_zero
                                    ((rawCast 2 + 0) ^ (n.primeFactorsList.length ^ rawCast 1 * rawCast 1) * rawCast 1 +
                                      0)))
                                (Mathlib.Tactic.Ring.zero_mul (rawCast 1 + 0))
                                (Mathlib.Tactic.Ring.add_pf_add_zero
                                  ((rawCast 2 + 0) ^ (n.primeFactorsList.length ^ rawCast 1 * rawCast 1) * rawCast 1 +
                                    0)))))
                          (Mathlib.Tactic.Ring.atom_pf ↑n)
                          (Mathlib.Tactic.Ring.sub_pf
                            (Mathlib.Tactic.Ring.neg_add
                              (Mathlib.Tactic.Ring.neg_mul (↑n) (rawCast 1)
                                (Mathlib.Tactic.Ring.neg_one_mul
                                  (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                    (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                                      (Eq.refl (Int.negOfNat 1))))))
                              Mathlib.Tactic.Ring.neg_zero)
                            (Mathlib.Tactic.Ring.add_pf_add_gt (↑n ^ rawCast 1 * (Int.negOfNat 1).rawCast)
                              (Mathlib.Tactic.Ring.add_pf_add_zero
                                ((rawCast 2 + 0) ^ (n.primeFactorsList.length ^ rawCast 1 * rawCast 1) * rawCast 1 +
                                  0)))))
                        (Mathlib.Tactic.Ring.neg_add
                          (Mathlib.Tactic.Ring.neg_mul (↑n) (rawCast 1)
                            (Mathlib.Tactic.Ring.neg_one_mul
                              (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                                (Mathlib.Meta.NormNum.IsInt.to_isNat
                                  (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                    (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                                    (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))))
                          (Mathlib.Tactic.Ring.neg_add
                            (Mathlib.Tactic.Ring.neg_mul (rawCast 2 + 0)
                              (n.primeFactorsList.length ^ rawCast 1 * rawCast 1)
                              (Mathlib.Tactic.Ring.neg_one_mul
                                (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                  (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                    (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                                    (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                                    (Eq.refl (Int.negOfNat 1))))))
                            Mathlib.Tactic.Ring.neg_zero)))
                      (Mathlib.Tactic.Ring.add_pf_add_lt (rawCast 2)
                        (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                          (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑n) (rawCast 1)
                            (Mathlib.Meta.NormNum.IsInt.to_isNat
                              (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                                (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                                (Eq.refl (Int.ofNat 0)))))
                          (Mathlib.Tactic.Ring.add_pf_zero_add
                            ((rawCast 2 + 0) ^ (n.primeFactorsList.length ^ rawCast 1 * rawCast 1) *
                                (Int.negOfNat 1).rawCast +
                              0)))))
                    (Mathlib.Tactic.Ring.sub_congr
                      (Mathlib.Tactic.Ring.pow_congr
                        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                        (Mathlib.Tactic.Ring.atom_pf n.primeFactorsList.length)
                        (Mathlib.Tactic.Ring.pow_add
                          (Mathlib.Tactic.Ring.single_pow
                            (Mathlib.Tactic.Ring.pow_prod_atom (rawCast 2)
                              (n.primeFactorsList.length ^ rawCast 1 * rawCast 1)))
                          (Mathlib.Tactic.Ring.pow_zero (rawCast 2 + 0))
                          (Mathlib.Tactic.Ring.add_mul
                            (Mathlib.Tactic.Ring.mul_add
                              (Mathlib.Tactic.Ring.mul_pf_left (rawCast 2 + 0)
                                (n.primeFactorsList.length ^ rawCast 1 * rawCast 1)
                                (Mathlib.Tactic.Ring.one_mul (rawCast 1)))
                              (Mathlib.Tactic.Ring.mul_zero
                                ((rawCast 2 + 0) ^ (n.primeFactorsList.length ^ rawCast 1 * rawCast 1) * rawCast 1))
                              (Mathlib.Tactic.Ring.add_pf_add_zero
                                ((rawCast 2 + 0) ^ (n.primeFactorsList.length ^ rawCast 1 * rawCast 1) * rawCast 1 + 0)))
                            (Mathlib.Tactic.Ring.zero_mul (rawCast 1 + 0))
                            (Mathlib.Tactic.Ring.add_pf_add_zero
                              ((rawCast 2 + 0) ^ (n.primeFactorsList.length ^ rawCast 1 * rawCast 1) * rawCast 1 + 0)))))
                      (Mathlib.Tactic.Ring.pow_congr
                        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                        (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)))
                        (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.pow_one_cast (rawCast 2 + 0))
                          (Mathlib.Tactic.Ring.pow_zero (rawCast 2 + 0))
                          (Mathlib.Tactic.Ring.add_mul
                            (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_one (rawCast 2))
                              (Mathlib.Tactic.Ring.mul_zero (rawCast 2))
                              (Mathlib.Tactic.Ring.add_pf_add_zero (rawCast 2 + 0)))
                            (Mathlib.Tactic.Ring.zero_mul (rawCast 1 + 0))
                            (Mathlib.Tactic.Ring.add_pf_add_zero (rawCast 2 + 0)))))
                      (Mathlib.Tactic.Ring.sub_pf
                        (Mathlib.Tactic.Ring.neg_add
                          (Mathlib.Tactic.Ring.neg_one_mul
                            (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                              (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                                (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                                (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                                (Eq.refl (Int.negOfNat 2)))))
                          Mathlib.Tactic.Ring.neg_zero)
                        (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 2).rawCast
                          (Mathlib.Tactic.Ring.add_pf_add_zero
                            ((rawCast 2 + 0) ^ (n.primeFactorsList.length ^ rawCast 1 * rawCast 1) * rawCast 1 + 0)))))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.ofNat 0))))
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Tactic.Ring.add_overlap_pf_zero (rawCast 2 + 0)
                          (n.primeFactorsList.length ^ rawCast 1 * rawCast 1)
                          (Mathlib.Meta.NormNum.IsInt.to_isNat
                            (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.ofNat 0)))))
                        (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
                  (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
              (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
                (Mathlib.Tactic.Linarith.lt_of_lt_of_eq
                  (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
                    (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                      (Int.add_one_le_iff.mpr (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 2 n) hn)))))
                  (neg_eq_zero.mpr
                    (sub_eq_zero_of_eq
                      (id
                        (Eq.mp
                          (Eq.trans (Mathlib.Tactic.Zify.natCast_eq._simp_1 (2 ^ n.primeFactorsList.length) n)
                            (congrArg (fun x => x = ↑n) (cast_pow 2 n.primeFactorsList.length)))
                          h)))))
                (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_le._simp_1 (2 ^ n.primeFactorsList.length) (2 ^ 1))
                        (congr (congrArg LE.le (cast_pow 2 n.primeFactorsList.length)) (cast_pow 2 1)))
                      a)))))))this:4 ∣ !n := Dvd.dvd.trans this✝ (dvd_of_mod_eq_zero h_mod)⊢ 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⊢ 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 thisAll goals completed! 🐙
  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 declaration uses 'sorry'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) = 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⊢ False
      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 < c omegaAll goals completed! 🐙) (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✝ aesopAll goals completed! 🐙)))
    rw [dvd_iff_mod_eq_zero, left_factorial, sum_nat_mod, ← sum_subset (range_mono hc')
      (by simp +arith +contextual [mod_eq_zero_of_dvd, dvd_factorial,
        pos_of_dvd_of_pos hc (factorial_pos _)])] 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