Post #2522104
2026-05-10 21:00 UTC
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
Replies (2)
-
@screwlisp@gamerplus.org 2026-05-10 21:12
@vnikolov@ieji.de That's what I mean when I say acl2 seems like a much better choice of target anyway! @kentpitman@climatejustice.social @bagder@mastodon.social
-
@kentpitman@climatejustice.social 2026-05-10 22:16
@vnikolov@ieji.de Well one of the strengths of LLMs is the ability to change formats,.. is that really the thing you worry about? cc @screwlisp@gamerplus.org @bagder@mastodon.social