Formal verification of the Euler Sieve via Lean

Abstract

This paper presents a formal verification of the Euler Sieve algorithm — a linear variant of the classical Sieve of Eratosthenes — using the Lean proof assistant. We begin by discussing the traditional Sieve of Eratosthenes and its inherent redundancy when crossing out composite numbers. We then introduce the Euler Sieve, which overcomes this drawback by ensuring that each composite number is “marked” only once, achieving linear time complexity. Finally, we present a Lean formalization that rigorously verifies the correctness of the Euler Sieve, including definitions, lemmas, and the overall rigorous recursive structure. To the best of our knowledge, this work is the first formal proof of the Euler Sieve by an interactive proof assistant.