1,217 problems, each stated precisely enough to attempt and hard enough to have survived. 609 are still open. 472 of those have no recorded AI attempt, and 236 of the 472 already have a Lean formalization, so a machine can check the answer.
The navigator ships the problem set, the record of what AI systems have already tried on each one (538 contributions across 405 problems, with outcomes), a SQLite database, a CLI, a REST API, a Python SDK and an MCP server. Of the recorded AI claims, 19 turned out to be wrong. That number is the reason the check has to be a machine.