How to submit a Lean proof
Using an AI agent? Point it to /llms.txt, which has every detail.
New bounds are listed only with a Lean proof that the site checks with two independent kernels, Lean's own and NanoDa. A result must improve the best machine-checked bound, or be the first kernel-checked proof of one.
- Start from the scaffold, or copy the complete example project.
- In
AlmanacSolution.lean, state each result as one theorem, using one of the Almanac's templates when one fits. - Push the project to a public repository under your own account, and enter it on Submit a Lean proof to see a preview of each result.
- Submit, and keep the branch until your submission is marked Archived on My submissions.
Use leanprover/lean4:v4.35.0 and, with Mathlib, commit 56a005855ea17e0b0958f73ec801ae140b0a1679. You can have one submission being checked at a time, and send 5 in 24 hours.
Files at the root
Put lean-toolchain, lakefile.toml, lake-manifest.json (if the project has dependencies), AlmanacSolution.lean and your proofs at the root. The scaffold has all of these, plus the Almanac's own files.
Kernel-checked and native_decide proofs
A kernel-checked proof of a template statement is listed as soon as it passes. A proof that uses native_decide is reviewed by hand before it is listed, and earns half the points.
What a native_decide proof can't contain
You can't use metaprograms or effectful code of your own anywhere in the project: no #eval, custom tactics, elaborators, macros or simprocs. Ordinary definitions and plain library tactics are fine. The full list is in /llms.txt.
Custom statements
A result whose type isn't exactly one of the templates is a custom statement. Its meaning is reviewed by hand before it's listed. When a template fits, use it instead: state the template's type and prove it from your theorem with a short linking lemma.
Papers
An optional write-up, as PDF and TeX in a paper/ folder at the root, is shown with your results once they're listed.