Post #2920388
2026-05-12 05:14 UTC
@dimpase@mathstodon.xyz @tao@mathstodon.xyz
by the way, someone asked me in this context why a formal proof written for a formal proof checker would need to be reviewed.
In this case I guess the answer is that a program of a valid proof needs to be checked that it is a formalisation of the informal description.
So validatable formal text of a proof technically existing somewhere does not mean anything if there is not a skilled human in the loop. The utf8 sequence of the proof will exist somewhere inside pi, right.
Replies (1)
-
@screwlisp@gamerplus.org 2026-05-12 05:18
@dimpase@mathstodon.xyz One can imagine that LLMs will eventually generate proofs that for computational burden reasons are uncheckable in practice. What will it mean if the LLMs did what they normally did, and say this is a valid proof, but in practice no human+computer is currently or soon going to be able to check. Alllsooo, if the formal logic is computer generated anyway, wouldn't a first order logic fully automatic theorem prover proof be infinitely better and equally easy i.e. #acl2 as #lean? @tao@mathstodon.xyz