Mathzoo is a user maintained collection of mathematical formalizations in the Lean theorem prover that are both standalone (a short file that depends only on mathlib) and deadend (nothing will ever depend on it). We call each such file a gem.

1. Minimal requirements. Gems will be accepted without detailed code review. There are no requirements on proof style or formatting conventions.

2. Minimal maintainance. Gems need not be kept up-to-date with mathlib. Files that no longer build must begin with a comment -- #mathlib YYYY-MM-DD <commit> indicating the last known commit against which the file builds.

3. Dataset friendliness. We strongly encourage the inclusion of metadata that will make gems more useful as training data for both mathematical problem solving (e.g. The IMO Grand Challenge) and auto-formalization.

Gems are organized in a directory hierarchy that reflects their provenance as much as possible. For example, a proof of the first problem from IMO 2021 lives at /src/olympiads/imo/2020/p2.lean while a solution to an exercise from the third chapter of the Concrete Mathematics textbook would live in /src/textbooks/concrete_mathematics/chapter3/. There may be multiple gems corresponding to different proofs of the same problem, in which case the filenames should be postfixed either with a description of the proof (e.g. p6_complex_bash.lean) or just an alternative number (e.g. p6_alt2.lean). As a rule-of-thumb, we suggest creating a sub-directory whenever there is a clear sub-category that might eventually contain more than (say) ten gems. Every directory includes a README.md file describing the source and linking to it as appropriate.

Every gem must:

• be in its own file
• build on the current version of mathlib (i.e. the version in leanpkg.toml)
• include a description of where the problem came from (if not implied by filename)
• only import files from mathlib and mathzoo's imports folder
• be sorry-free
• be example-free
• be reasonably short (e.g. <200 lines, not including comments)
• compile within a reasonable amount of time (e.g. 1 minute in CI)
• not produce any output

We do allow gems that consist of a formal statement without proof, in which case the statement should appear as an axiom declaration.

We also encourage gem-writers to include:

• an informal statement of the problem (if not easily accessible online)
• links to any proofs consulted during the formalization
• ideally: detailed comments aligning an informal proof to the formal one

Note: the -- #mathlib YYYY-MM-DD <commit> header will be added automatically to files that break when updating mathlib, by the script update_mathlib.py.