As someone inexperienced (as compared to friends and colleagues who do this for a living on much bigger projects) with formally verifying software for correctne

As someone inexperienced (as compared to friends and colleagues who do this for a living on much bigger projects) with formally verifying software for correctness I have similar thoughts on the matter. When it matters that the answer is correct with regards to a specification you need to be very precise with your specification. We would like to be able to have a genie in a bottle, so to speak, that can take our ill-formed thoughts and "do what we mean," but if you cannot state your specifications precisely you should expect that any program implemented is going to be, "kind of right some times." However, an LLM is going to be severely hampered at proving that it's solution is correct with regards to such a specification when it comes to software. As you demonstrate with your series of prompts it can't discern the truth of an expression by reading more input. It's all "meaningless" in a certain sense to the LLM: highly contextual, interconnected meaninglessness. I think it will take more work in this area for a future model, possibly based on LLMs, to be able to reason with axioms and deduction; to "know" when it should derive an expression to make the following reasoning more clear to future readers, etc. In some ways it is much like a genie... if you don't give it a precise specification then any program could be correct in some way. In a sense you get what you wish for.