Method

Each paper goes through three stages:

1. Formalisation. One or more contributors pick a paper and formalise its results in a proof assistant (Lean, Rocq, Isabelle, Agda, etc.). The code is hosted in a public repository. AI may be used but must be disclosed.
2. Audit. One or more contributors check whether the formalisation faithfully captures the paper's content and write an audit report recommending whether to accept or reject it, with argumented justification. Auditors must differ from the formalisation authors, unless the formalisation was done by AI. AI may assist, but the human authors of the report are fully accountable for its conclusions.
3. Acceptance. Admins follow the recommendations of the audit report, unless they determine that the human-accountability criterion of the report is not satisfied, in which case the report is discarded. Accepted formalisations count toward the project's formalisation goal. Rejected formalisations go back to stage 1 so that their authors can address the problems.