SAIR competition – Lean Kernel Challenge

We’re excited to launch Stage 1 of the Lean Kernel Challenge, a multi-stage competition to improve the performance of verified computation in the Lean 4 kernel that the whole community can benefit from. The Lean Kernel Challenge brings the community together to develop faster algorithms and better representations for verified computation. Through these collective contributions, the competition aims to support Lean’s development and benefit Lean users worldwide. Verified computation uses the Lean kernel to check computational results as part of a proof. Stage 1 is the first, experimental stage of the series, beginning with fundamental problems. Later stages will cover a broader range of mathematical and scientific fields and more complex problems. The Lean Kernel Challenge is inspired by the Lean Kernel Arena, and we thank its contributors. Lean Kernel Arena benchmarks alternative Lean proof checkers; the Lean Kernel Challenge focuses on algorithms and representations for verified…