@vnikolov@ieji.de 1. I have only seen lean ones. I think I have seen people mentioning not-using-lean though. I would have thought a tool like the acl2 fully automatic theorem prover would have been more powerful. 2. 1. Well in the problem 728 one the mathematician said chatgpt did it on its own, except when it went in a useless direction in which case the mathematician resteered it. 2. 2 I don't personally use lean, to be fair. @kentpitman@climatejustice.social @bagder@mastodon.social