@solrize@mathstodon.xyz - theory building involves a lot of choosing good definitions... and ideally all the theorems you want become easy, but it rarely works that way except in category theory, which is like math without friction. Scholze is a signatory of the Association for Human Mathematics, which calls for mathematicians to avoid AI: https://www.ahmath.org/