Post #2920389

@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