Li, I. (Rucheng). Formal Verification of the Euler Sieve via Lean. Pittsburgh Interdiscip. Math. Rev. 2025, 3, 82-101.