SAIR competition – Lean Kernel Challenge

It launches a multi-stage competition aimed at improving the performance of verified computation in the Lean 4 kernel, where verified computation uses the Lean kernel to check computational results as part of a proof. Unlike the Lean Kernel Arena, which benchmarks alternative Lean proof checkers, this challenge focuses on algorithms and representations for verified computation, and Stage 1 uses fixed tasks evaluated by a fixed Lean kernel. The announcement states that it is inspired by the Lean Kernel Arena and thanks its contributors, and it describes the difference in focus; no performance data or evaluation results are given.

Stage 1 specifies eight problems: Fibonacci, integer partitions, the Mertens function, prime counting, matrix permanent, Rule 110, SHA-256, and polynomial discriminant. It offers a public, fixed problem list as a shared starting point for community work, spanning number theory, combinatorics, linear algebra, cellular automata, and cryptographic hashing. The problem list is given directly in the announcement; the announcement does not state input sizes, scoring rules, or baseline implementations.

Participants are asked to develop an algorithm for each problem and to prove in Lean that it matches the supplied specification for every input. It ties algorithmic efficiency and a formal correctness proof into a single submission requirement, rather than comparing running speed alone. The announcement states this requirement in a single sentence; it does not describe how proofs are checked, which assumptions are allowed, or which libraries may be used.

The competition is co-organized by Lean FRO and the SAIR Foundation, with an organizing committee of Joachim Breitner, Leonardo de Moura, Kim Morrison, and Terence Tao, and it provides a competition site, an SAIR Playground, and an official repository. It supports community participation through public infrastructure (submission entry point, playground, and repository) where participants can obtain tasks and submit work. The announcement lists the organizers, committee members, and three links; it does not describe prizes, the review process, or how results will be announced.

The scope defined by this announcement is verified computation in the Lean 4 kernel, with Stage 1 being the first, experimental stage that begins with fundamental problems; later stages will cover a broader range of mathematical and scientific fields and more complex problems. It is aimed at participants willing to write algorithms in Lean and complete formal correctness proofs, with a submission deadline of November 20, 2026, 23:59 AoE (UTC−12).

The announcement does not state the input sizes or scoring criteria for each problem, the specific configuration of the evaluation environment, whether external libraries or axioms are permitted, or the prize and review arrangements, and it gives no baseline performance or prior results. In addition, the text read here is blog page content and does not include the task details on the competition site, the Playground, or the code repository, so the specific specifications and acceptance criteria for each problem still need to be confirmed through official channels.