> But now that it’s letting everyone
Eh... That “everyone” is a multi billion (trillion?) $ company paying top mathematicians specifically hired for generating math proofs.
No, pretty much every math PhD student and researcher is now using the AI+lean combo.
No, pretty much every math PhD student and researcher is now using the AI+lean combo.