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 computation, beginning in Stage 1 with fixed tasks evaluated by a fixed Lean kernel.

Stage 1 features eight problems: Fibonacci, integer partitions, the Mertens function, prime counting, matrix permanent, Rule 110, SHA-256, and polynomial discriminant.

For each problem, develop an algorithm and prove in Lean that it matches the supplied specification for every input.

Submission deadline: November 20, 2026, 23:59 AoE (UTC−12).

Competition and submissions:
https://competition.sair.foundation/competitions/lean-kernel-challenge

SAIR Playground:
https://playground.sair.foundation/playground/lean-kernel-challenge

Official repo:
https://github.com/SAIRcompetition/lean-kernel-challenge

Thank you for participating and supporting SAIR competitions!

Co-organized by Lean FRO and the SAIR Foundation.
Organizing committee: Joachim Breitner, Leonardo de Moura, Kim Morrison, and Terence Tao.