Not bad as a list of problems to solve, but this isn’t what people normally mean by a theorem prover. In the usual concept, the input to the theorem prover is already formalized. You need something like a higher-powered version of Wolfram’s proposed coupling between ChatGPT and Wolfram Alpha.
Not bad as a list of problems to solve, but this isn’t what people normally mean by a theorem prover. In the usual concept, the input to the theorem prover is already formalized. You need something like a higher-powered version of Wolfram’s proposed coupling between ChatGPT and Wolfram Alpha.