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.

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.

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 (90 good tests, 46 bad tests, 2.3 MB). The tarball contains subdirectories good/ and bad/ based on expected results, making it easy to test your own checker implementation.

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.