Make Lean Pool projects academically citable (DOI / ORCID / companion notes)

[Vilin97]

Motivation

Make each Lean Pool project academically citable so that contributing a formalization earns real academic credit. Citability is the incentive flywheel: if authors get credit, they want their work in the pool, and Lean Pool sources itself instead of relying on manual discovery.

Components

• DOI per project via Zenodo (free, CERN-run; archives a frozen snapshot). The monorepo layout means minting per-project DOIs through the Zenodo API rather than its per-repo GitHub integration. Use Zenodo "concept DOIs" so a project identifier survives Mathlib bumps.
• Citation metadata in projects.yml — it already carries title / authors / source / MSC. Add doi and per-author orcid fields so projects.yml stays the single source of truth.
• Generate citation snippets (BibTeX + CITATION.cff) from projects.yml.
• Surface citations — show authors, DOI, and a copy-paste "How to cite" block on each project's doc-gen4 page and README card.
• ORCID — semi-automatic via Zenodo -> DataCite -> ORCID auto-update once an author authorizes it. Low effort; treat as a CV listing, not a prestige credential.
• Companion notes for real credit — Google Scholar indexes documents, not repos or bare DOIs. Projects wanting genuine academic weight need a short write-up (2-6 pp., arXiv or PDF with citation_* metadata). Ties into the broader paper effort.

Notes

Anti-abuse / credibility: the credit is backed by machine verification plus the review gate, not by gaming an index. The significance bar in .github/REVIEW_RULES.md keeps per-project DOIs from looking like padding.

[github-actions]

This issue has been inactive for 90 days and is marked stale.