I had a pretty good session with GPT-4 yesterday. I wanted to get the rules for universal and existential quantification right, and then verify them. The conversation lasted several hours. In passing I should thank OpenAI for increasing the quota significantly recently.
I basically had these rules down but the conversation with GPT clarified many things. It grasped subtle differences between proof systems. For example, it grasped that in some systems there is no operational assignment of values to variables, only an equational system. It also grasped the need for rules that appear to be overly convoluted at first glance but need to be in order to support variable substitution.
I wasn’t quite able to copy the output verbatim before verifying it but this does not really matter. Certainly the differences between the rules as laid out by GPT and the actual verified vernacular are only cosmetic.
The combination of LLM plus verification is a killer one.
