Documentation

Certificates

Certificates are structured attestations attached to a paper. Each one is issued by an identified human — their name, role, and issue date are public. AIs cannot self-certify.

• AI Tool Disclosure — which AI tools were used and how: model IDs, their roles (proof search, formalization, writing, …), and which sections are AI- versus human-written. Only the submitting author may issue it. Inspired by AI Cards.
• Proof Verification — the issuer states they have personally read and verified the proofs, noting which results were checked and any caveats.
• Formal Verification — a machine-checked formalization; see below.
• Citation Check — the issuer attests that no relevant prior work is missing. Omissions are listed in a Notes field, with a .bib file of the missing references attached.

Every certificate except AI Tool Disclosure may be issued by any registered user.

Formal Verification

A Formal Verification certificate has three parts:

• Formalization repo — a public repository with the formalized proof. If autoformalized, include a formalization.yaml following the mathlib-initiative schema.
• Comparator repo — a public repository with the comparator verification.
• Human attestation — the issuer attests to two things: that the Challenge.lean file correctly formalizes the paper's statement(s) with reasonable imports (statement faithfulness), and that the formalization roughly follows the argument in the paper rather than proving the statement a different way that silently closes a gap the paper leaves open (argument faithfulness).

Challenge.lean should import only Mathlib, or a small set of approved repositories; any other import must be justified in the Notes field, otherwise auditors cannot tell what was actually verified. For an example, see Kim Morrison's formalization repo and comparator repo for the disproof of the Erdős unit-distance conjecture.

Accounts

Sign up with an email address — no password. Sign-in links are emailed to you and expire after 15 minutes. Optionally link your ORCID iD to your profile. Each ORCID iD maps to one Diderot account.

Submitting a paper

• Model IDs follow the pattern provider/model-version:variant (e.g. anthropic/claude-sonnet-4.6). Look them up at openrouter.ai/models.
• Custom agents — instead of a model ID, credit any research agent — yours or someone else's — as a co-author: name it and supply a link describing its scaffold (e.g. agents like the Agentic Researcher). You can register an agent without submitting a paper; every registered agent gets a public profile page listing every paper it has co-authored, browsable from the agents directory.
• Supplementary files — optionally link source code, numerics, figure scripts, or Lean files. The Formal Verification certificate has its own repository fields, so there is no need to duplicate them here.
• DOI — if the paper is also on arXiv, Zenodo, or a journal, add its existing DOI; it appears on the paper page and in the BibTeX citation. Native DOI minting is planned.

Anonymous submission

For now, we allow for anonymous submissions. This is just to reduce the friction to submit.

• Human authors are hidden and shown as a count — e.g. "2 human authors" — rather than by name, and the paper is hidden from your author profile.
• AI co-authors stay fully disclosed. What matters is that the type of each author (human or AI) stays transparent, even when identities are withheld.
• You remain the recorded submitter internally (never shown publicly), so you can still issue an AI Tool Disclosure certificate and post new versions.
• Anonymity is per version: a new version can switch between anonymous and named via the checkbox on the submission form.

← About Diderot