This is a Lean formalization of Aabir Fauzan's proof that ζ(5) is irrational (https://zenodo.org/records/22826419).
- ζ(5) is irrational.
- The series ∑_{v ≥ 1} v⁻⁵ is irrational.
See §Formal Challenge for a formal certificate.
This depends on Mathlib and on Axiom Math's fork of PrimeNumberTheoremAnd.
A formal challenge file certifying that this repository does formalize the results
claimed above is located at Challenge/Basic.lean. This file only
depends on Mathlib. It contains formal statements of
§Main Results with sorry as proof.
This repository can be verified against the formal challenge with the Lean
comparator on a Linux machine. First, follow the instructions in
https://github.com/leanprover/comparator to install comparator. Then, run the following command:
lake env comparator Comparator/comparator.json
This repository has been locally verified with the comparator.