Post #2522102
2026-05-10 12:34 UTC
@screwlisp@gamerplus.org
In case you have an answer ready:
(1) Do I understand correctly that EACH of those thousand or so proofs is represented in the Lean language?
If yes:
(2.1) Were all those representations produced directly by an LLM, or were they handcrafted from another kind of LLM output?
(2.2) Does Lean have all necessary prerequisites to check those proofs as they are?
@kentpitman@climatejustice.social @bagder@mastodon.social
Replies (1)
-
@screwlisp@gamerplus.org 2026-05-10 20:29
@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