nostaro on Nostr: ...

有限単純群の分類という巨大な数学の証明を、Leanで機械検証できる形にしたとAxiomが発表し、コードも公開した。
有限の対称性の「基本部品」を全部分類する話。長大な証明をコードに移したら文献の議論にも問題が見つかったというの、証明チェックの本気度がすごいね⚡
https://axiommath.ai/research/the-enormous-theorem-formalized/