Contribute

How to help the project

Steering

See About: Steering for the committee and project maintainer. Project support is distinct from review of an individual claim.

Supporting the project

The project’s stated aim is to advance the field collaboratively with the help of AI, and to disseminate the results: remove the low-hanging fruit and move to the next layer as AI advances. (See the statement on the Philosophy page.)

Participants can help in multiple ways:

  • Steering. Help establish the direction of the project, and widen participation among colleagues and students.
  • Conjecture formulation and resolutions. Open questions from your own work or others’, stated precisely, then proved or disproved.
  • Formalizations. Formalizing statements and proofs in Lean and other ITPs.
  • Reviewing. Review the correspondence between informal and formal statements, and help prioritize problems by significance and difficulty.
  • Contributing tokens. Pooled, distributed compute capacity from idle tokens.
  • Website and workflow maintenance. The site, its build, and the scripts and prompts behind it — building a coherent website and the tooling around it.
  • Ideas! How the archive should be organized, what a statement’s page owes a contributor, which conventions are wrong. Open a PR, or say so on Zulip.

Skills needed

Contributing does not require all of these, and it does not have to be mathematical. The archive is a research object and a piece of software at once, so it needs both kinds of help.

  • Cryptography and theory. Reading a paper closely enough to extract what is actually open, and stating it precisely.
  • Formalization. Lean 4 and Mathlib, or other theorem provers, formal methods and DSLs, and judgement about when a formal statement faithfully renders an informal one.
  • Developer tools. git and GitHub Actions, bash, VS Code, and the ordinary discipline of small reviewable pull requests.
  • Web architecture. Quarto, static site builds, HTML and CSS, MathJax, client-side search, accessibility, DNS and hosting.
  • AI agent tooling. Claude Code CLI, CLAUDE.md, skills (SKILL.md), MCP servers, hooks and subagents, and the design of prompt harnesses whose runs are reproducible rather than merely impressive.
  • Bibliography and metadata. BibTeX hygiene and citation resolution against Crossref, DBLP and IACR ePrint.
  • Editorial and design. Typography, page structure, and the house style a statement page is held to.

If you have one of these and none of the others, that is enough. Say so on Zulip or open an issue.