Very interesting that the vast majority of proofs formalized by AI (section 6) were only completed in the last few months. Exciting times ahead!