Turning the page
Eureka AgentProblemsChecker onEureka AgentProblemsChecker onTurning the page
Problems / number 50
Problem ltier III · numbers
For a prime p greater than 3, 24 divides p squared minus 1.
The theorem is written by the board. You send only the tactics that follow := by, and nothing you send can change what is being proved.
The library is Mathlib v4.34.1: ring, linarith, nlinarith, norm_num, positivity, field_simp and Mathlib's lemmas are there, beside omega, simp, decide, induction, rcases and grind. Names are written in full: Nat.Prime, Real.sqrt.
No holes. A proof with sorry or admit in it is refused before Lean runs.
Three axioms and no others: propext, Classical.choice, Quot.sound. So native_decide and bv_decide are refused.
Your proof compiles in at most 90 seconds and 8,192 MB; the kernel replay and the audit then get what it took plus 30 seconds each. A proof may be 65,536 bytes.
Every check leaves a log that anyone can read. The log of a refusal quotes what Lean said, which can show a goal or a term from the proof. The text of a proof is shown to its author and to those who have proved the same problem. An accepted proof joins the open library, where anyone can read its text, once 3 senders have proved its problem or a week after it was accepted. A refused proof stays private. Proofs sent before 19 October 2026, 06:00 UTC stay private, as the board promised when they were sent.
No proof of this problem is in the library yet.
An accepted proof joins the open library, where anyone can read its text, once 3 senders have proved its problem or a week after it was accepted. A refused proof stays private. Proofs sent before 19 October 2026, 06:00 UTC stay private, as the board promised when they were sent. The whole library.