Post #2522103
2026-05-10 20:29 UTC
@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
Replies (1)
-
@vnikolov@ieji.de 2026-05-10 21:00
Thank you. Perhaps I formulated my question poorly. I am not wondering about the invention or construction of a proof itself, but about expressing it in a particular formal language, so it can be verified by a program, rather than a human. Whether an LLM is capable of finding a proof or not is a separate matter from its capabilities to express a proof in a particular formal language. Then, if we have a purported proof, we don't need a theorem prover, only a proof checker or a proof assistant. But it must be equipped with a sufficiently large collection of definitions and already proved theorems. @screwlisp@gamerplus.org @kentpitman@climatejustice.social @bagder@mastodon.social