Lean Kernel Arena

The Lean Kernel Arena presents, tests and benchmarks proof checkers for the Lean Theorem Prover.

The data above is generated by running each checker on a suite of test inputs. Test inputs are either valid proofs that should be accepted (column 👍), or invalid proofs that should be rejected (column ✋). The checkers are scored based on their ability to correctly accept and reject these tests.

The time and space measurements refer to the mathlib test case, the largest correct test in the suite. The ⏱️ column shows virtual CPU time, calculated from instruction counts using a fixed rate of 6.0 Ginstr/s. This provides consistent performance comparison across different hardware, though it does not reflect parallel processing capabilities that some checkers may use.

For performance-compared tests (such as the perf/ group), the cells show the runtime relative to the official checker. A dark green background marks the fastest checker for that test, and a light green background marks checkers that are at least 10% faster than the official checker.

Checkers that do not implement all features may choose to explicitly decline to process certain tests (column 🚫). These tests are not taken into account for correctness scoring. Tests that crash the checker (💥) also considered declined.

Tests can come without an expected outcome (shown as 🤷). These test corner cases that are not known to be soundness relevant and not typically relevant in practice, and where it is acceptable for a checker to accept or to reject. They are excluded from the completeness and soundness scoring.

For more details on the interface for external checks, and how to submit these, see the project's README.md file.

A tarball of the test suite (excluding tests larger than 10 MB) is available for download: lean-arena-tests.tar.gz (116 good tests, 62 bad tests, 2.6 MB). The tarball contains subdirectories good/ and bad/ based on expected results, making it easy to test your own checker implementation.

The raw data behind this page is available as results.json (2.5 MB). It contains the checker metadata (checkers), the test metadata (tests) and the array of all individual results (results), and may be useful for further analysis of the data.

The test suite includes a set of tutorial test cases that exercise individual features of the Lean type system step by step, from basic definitions through inductives, recursors, projections, definitional equality rules, and quotient types. Each tutorial test is a small self-contained environment, making them a useful starting point for developing and debugging a new kernel checker.

We are interested in extending our test suite, in particular tests that should be rejected are a useful help for authors of new kernel checkers.