FormalPantheon collects our formalization projects across different areas of mathematics.
- BoundedGaps: A Lean formalization of bounded gaps between primes, based on James Maynard's Small Gaps Between Primes and the breakthrough of Yitang Zhang's Bounded Gaps Between Primes, with the Bombieri--Vinogradov (BV) theorem as a central intermediate theorem.
- Period Three: A Lean formalization of Li and Yorke's Theorem I and its period-three-implies-chaos corollary, from T.-Y. Li and J. A. Yorke's Period Three Implies Chaos (American Mathematical Monthly 82, 1975).
- Warning: A Lean 4 formalization of Chen Jingrun's theorem that every positive integer is a sum of at most 37 fifth powers of nonnegative integers, and that 37 is the smallest such uniform bound, based on Chen's Waring's Problem for g(5)=37 (Scientia Sinica 13, 1964).