Lax Lean Archive

Formalized mathematics that can be read, checked, and built upon.

Lax is an open archive for contemporary mathematics written in Lean. Think of it as an arXiv for formalization: independent, citable submissions that people can read, software can check, and future work can build upon.

Read the Lax paper

What you can do here

Cite.Every page carries a ready-made BibTeX entry.

Contribute to Lax

Creating your own submission

Contributing is a two-step process.

  1. Set up, once per machine:

    npm install -g lax-archive
lax doctor    # checks your setup and installs whatever is missing

  2. Hand your coding agent a prompt like:

    Run `lax print instructions` and follow the guide it prints
to formalize <my result>.

Prefer to work hands-on, or want to know what happens at each step? See Getting started.

Read the archive

Submissions

42 submissions · 445 concepts · 310 statements, 285 proven

Browse by topic

Suggested from submission and concept titles.

Showing all 42 submissions.

Contribute a review

Review a concept

Used by 2 other submissions and 9 other concepts

Nowhere dense graph classes

This concept is reused elsewhere in the archive. Review its mathematical correctness, endorse it if correct, or flag a flaw.

Review now

Contribute a proof

Open proof obligations

Browse every claim that does not yet have a grounded proof, across 3 submissions.

25 proof obligationsBrowse proof obligations

About Lax

FAQ

  1. How does Lax relate to projects such as Merely True and Tau Ceti?

    In Merely True and Tau Ceti, individual contributions blend into a shared library. Lax keeps each submission as a distinct, citable unit. This is closer to academic publishing culture: a submission can be cited directly or attached — anonymously, if needed — to a conference or journal submission for review.

    Like Lean Pool and the Palomar Registry, Lax archives individual submissions. The important difference is that Lax submissions can build on one another. A base submission might define a concept such as treewidth; later submissions can cite and import it instead of asking the community to vet the same definition again.

  2. How can Lax help with conference and journal review?

    A paper accompanied by a Lax submission gives reviewers a shorter route to checking that its formal statements are correct. Lax exposes the semantic closure of each statement: the definitions, assumptions, and results on which it depends. Reviewers can therefore focus their limited time on the ideas and techniques, while readers can inspect full proofs whenever those details matter to them.

  3. Can I use Lax for anonymous peer review?

    Yes. List the author as Anonymous author and keep the submission in draft mode during review. You can replace the placeholder with the real author name before registering the final, permanent version.

  4. Can I work on two submissions in parallel locally?

    Yes. Keep each submission in a separate repository checkout or Git worktree, then run Lax from the corresponding project directory. That keeps each submission's manifest and working tree independent while sharing the installed toolchain.

  5. Which operating systems does Lax support?

    Lax is tested on Linux and macOS. On Windows, use the Windows Subsystem for Linux (WSL); native Windows support is not currently tested.

  6. Does my submission need to be hosted on GitHub?

    No. Lax accepts submissions hosted on GitHub, GitLab.com, Codeberg, and Bitbucket Cloud. If your preferred Git host is missing, contact the Lax team so support can be considered.

  7. How do dependencies stay compatible as mathlib changes?

    Submissions that build on one another need compatible Lean, mathlib, and other dependency versions. Lax therefore plans to use long epochs that freeze those versions across the archive. When a new epoch is needed, the community can carry useful submissions forward based on demand: if you build on something, help bump it. Epoch length will follow how the archive and its community evolve.