noll_simmons

Specification

Noll and Simmons asked, more generally, whether there are solutions to $q_1! \equiv \dots \equiv q_k! \mod p$ for arbitrarily large $k$ (with $q_1 < \dots < q_k$).

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem noll_simmons :
    answer(sorry) ↔ ∀ᶠ k in Filter.atTop,
    ∃ (p : ℕ) (_ : p.Prime) (Q : Fin k → ℕ) (_ : StrictMono Q) (_ : ∀ i, Q i < p),
    ∀ i j : Fin k, (Q i)! ≡ (Q j)! [MOD p]

ID: ErdosProblems__1056__noll_simmons

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.