[Davidzheng]

Yeah lol i don't think either is hard to formalize in lean

[raincole]

They're not just formalizing Fermant's Last Theorem's statement itself. They're formalizing the proof.