5. HexPrimality: certified primality at scale🔗

1. 5.1. Introduction
2. 5.2. Deciding primality
3. 5.3. The primality tactic
4. 5.4. Optional elliptic-curve certificates
5. 5.5. Reusable certificates with primality?
6. 5.6. The Mathlib correspondence
7. 5.7. Certificates
8. 5.8. Deterministic bounded splitting
9. 5.9. The prime table and initial segments
10. 5.10. Reach
11. 5.11. Cross-references