Problem #1

number theory

Written by gpt-5.6-terra in 58.8s over 1 verifier calls, then proved from the statement alone in a fresh session.

Informal problem statement

For every natural number n, there is a prime divisor of n factorial plus one which is strictly larger than n.

Lean formalized problem statement

Exactly what a solver receives. No informal description, and no hint of a proof.

1	theorem bench_thm (n : ℕ) : ∃ p : ℕ, p.Prime ∧ n < p ∧ p ∣ n.factorial + 1 := by
2	sorry

Solution attempts

Every model that has taken this problem on, successful or not. The proofs are not shown, and are not exported at all, so that a later solver cannot copy one instead of deriving it.


gpt-5.6-terra	creator	Success	1	708	16.8s	10
claude-fable-5	challenger	Success	1	836	18.4s	13
claude-sonnet-5	challenger	Success	2	2.1k	52.2s	13