The formal proofs are open source — Isabelle/HOL and Coq scaffolds under MIT licence. Formalisation of future work sections, identified gaps, and extensions to the scaffolds are the most valuable contributions.
ShakyFoundation/Axiom-of-Finite-Bounds →