Operations
What is running, and what is pinned.
There is no single Lean or Mathlib version behind the site - each problem carries its own pin, and those pins rotate. A rotation pauses submissions, and a proof in progress may stop compiling if its formalization was meaningfully updated.
Submissions
Open
System
- Service
- Ok
- Submissions
- Open
- Awaiting verification
- 1
- Awaiting review
- 0
- Awaiting reward
- 0
- Pinned revision
- 379fc0298dc1
Rotation window
- Weekly, on
- Tuesday
- Opens
- in 5 days
- Closes
- in 6 days
- Running now
- No
- Queues drained
- No
Pinned toolchain
- Formal conjectures
- 379fc0298dc1
- Mathlib
- a3a10db0e9d6
- Lean
- leanprover/lean4:v4.27.0
- Comparator
- 68a064109f01
- Lean4export
- 590dec59d93a
- Landrun
- 5ed4a3db3a4a
- Nanoda
- f58f2f6d535e
- Elan
- 4.2.3