> 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.

	▲	geraneum 42 minutes ago \| parent [-]
		So as every high schooler. That doesn’t mean much for actual results similar to what OpenAI “generated”, and doesn’t quite explain the “war footing”, does it? We’ve yet to see the democratizing fantasies in math field to materialize.