Method

A contributor picks a paper from the literature and writes a formal proof in a proof assistant of their choice (Lean, Rocq, Isabelle, Agda, etc.). The formalisation is hosted in a public repository. AI tools may be used, partially or fully, but their use must be disclosed.

Once a formalisation is ready, one or more auditors review it to assess whether it faithfully captures the content of the original paper. Auditors must be different from the formalisation authors, unless the formalisation was essentially done by AI (autoformalisation). Auditors write a report explaining their findings. AI may assist the audit, but the human authors of the report must be fully accountable for its conclusions.

Admins assess the human-accountability criterion of the audit report in order to mark the formalisation as accepted. The paper then counts toward the project's formalisation goal. If the audit report found issues and recommends rejection, the formalisation goes back to the formalising stage so that the formalisation authors can address the problems.