Skip to content

CONTRIBUTING.md

Latest commit

 

History

History
29 lines (19 loc) · 2.42 KB

CONTRIBUTING.md

File metadata and controls

29 lines (19 loc) · 2.42 KB
Raw

Contributing

Contributions are welcome from anyone interested in formalizing the Stacks Project: new formalizations, reviews of existing ones, and better proofs.

Claim before you start

New formalizations and reviews are claimed before they start, so that efforts do not collide.

  1. Find a task on the task board, or a Stacks tag in the library, and check the open claims.
  2. Open a claim with a blueprint: the exact statement, the Lean statement you intend to prove, the declarations in this library or in Mathlib that you will use or extend, and a proof outline. The task board pre-fills this for you.
  3. A maintainer reviews the blueprint in the issue. When it is approved, the issue is labelled blueprint-approved and assigned to you. That is your claim.
  4. Formalize it and open a pull request that closes the issue.

Improvements to existing proofs and small fixes (typos, broken proofs, documentation) do not need a claim; open a pull request directly.

The two tiers

  • StacksCore: formalizations checked against the Stacks Project and brought to Mathlib standards of naming, generality and style.
  • StacksFrontier: everything else, including AI-assisted formalizations. Moving code from StacksFrontier into StacksCore, after checking that its statements faithfully capture the source, is one of the most useful contributions.

Every pull request, to either tier, is reviewed by the maintainers: Kenny Lau, Brian Nugent, Ashvin A. Swaminathan and Yunzhou Xie.

Conventions

  • Attach @[stacks TAG] to the declaration that formalizes a tag. If it covers only part of the tag, say which part in the attribute's comment, for example @[stacks 00DS "part (1)"]. Register a tag that Mathlib already covers with add_to_stacks.
  • State the result the Stacks Project states, in its generality. Do not weaken a statement to make it provable; if a statement is wrong, say so in the claim.
  • Place each file in the module matching its mathematical topic, and reuse existing definitions rather than introducing parallel ones.
  • No sorry, admit, native_decide or new axiom. #print axioms on your results should list only propext, Classical.choice and Quot.sound.
  • Follow Mathlib's naming and style conventions.