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.