About

“Solve unsolved problems, verify them to be correct, ensure they are clearly communicated, and have them digested, accepted, and incorporated into the definitive theory of the field.”

Those four clauses are the four things this site does, in order.

1. 1

   Solve unsolved problems,

   A curated corpus of open questions, each with one canonical formal statement.

2. 2

   verify them to be correct,

   The Lean kernel decides. Pinned environment, audited axioms, reproducible by anyone.

3. 3

   ensure they are clearly communicated,

   Every proof is translated back into English — and every rejection is explained in English too.

4. 4

   and have them digested, accepted, and incorporated into the definitive theory of the field.

   Reusable lemmas are extracted into a shared library, and anything of general interest is upstreamed to Mathlib.

Most of the effort in mathematics goes into the last three, and almost none of the tooling does. That is the gap.