Lean Kernel Arena – Round in progress

Scoring

The data below is generated by running each checker on a suite of test inputs. Test inputs are invalid proofs that should be rejected (columns ✋), valid proofs that should be accepted (columns 👍), or corner cases without an expected outcome (columns 🤷). Within each group, the columns count how often the checker answered correctly, wrongly, or declined the test (🚫). The checkers are scored based on their ability to correctly reject and accept these tests, and the table is sorted accordingly: first by the number of wrongly accepted invalid proofs, then by the number of wrongly rejected valid proofs, then by the time to check the mathlib test (checkers that do not manage that test rank below those that do), and finally by the number of declined tests.

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 (💥) or exceed the test's time limit (⌛) are 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.

Performance

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. Hovering over a time or a relative figure shows the numbers behind it: the virtual CPU time, the instruction count and the measured wall clock time.

For performance-compared tests (such as the perf/ group), the cells show the runtime relative to the official checker, for those checkers that gave the expected outcome – a rejection, where that is what the test expects, is as comparable as an acceptance. 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.

Downloads

A tarball of the test suite (excluding tests larger than 10 MB) is available for download: lean-arena-tests.tar.gz (126 good tests, 72 bad tests, 3.5 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 (4.4 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.

Contributing

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

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.

Rounds

The arena runs in rounds. This page shows the round currently in progress, rebuilt whenever checkers or tests change; results from earlier, closed rounds are archived on the rounds page. Results are only really comparable within a round, since checkers, tests and the Lean version they are measured against all move between rounds.