This question can be interpreted many ways:
- Can ChatGPT produce valid Lean code if used naively?
- Can ChatGPT produce valid Lean code if used smartly?
- Can ChatGPT produce valid Lean code if hooked up to an API that was especially designed to use ChatGPT (or another LLM) to produce Lean code.
The answer to (1) is that it will likely fail if used naively. ChatGPT isn't aweful, but it will likely make lots of mistakes unless it is a simple proof. Sometimes, like in your case, the proof is actually a bit tricky to put into Lean.
n * (n+1) / 2 in Lean is a natural number and
/ is natural number division (so it takes the floor of the division). But I bet your proof is hard to translate directly into Lean because of this.
For (2), it is well known that these systems are a lot more powerful if you know how to talk to them the right way. First, the Chat in Bing is probably better since it is GPT-4 whereas the regular ChatGPT is GPT-3.5 (or so). Next, ChatGPT is designed for back and forth conversation. So if it isn't getting it right (like it is missing imports or there is an error), tell it. Just like Stack Exchange, it is helpful to be clear, and provide it with the right information and what you think is going wrong. Remember, ChatGPT doesn't have access to a Lean interpreter or the Lean library (well, maybe Bing has access to the library). If you and ChatGPT work together, you might be able to solve it as a team. Here is one example of that happening with GPT-4: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/GPT/near/341914198
For (3), note this is an active and exciting area of research. Can we use LLMs to translate informal math to formal math, solve formal proofs, and otherwise generally help with interactive theorem proving? A year ago, those of us who research this would have been quite doubtful. But this field is moving quite fast. Since that time the following papers and research projects have come out. They aren't anywhere close to 100%, but I see a lot of potential here.
- Autoformalization with Large Language Models
. Uses Codex (a precursor to ChatGPT and the model behind Github copilot) to translation math theorem statements into Isabelle/HOL with about 25% accuracy. Here is a Quanta article on this.
- Lean Chat. Based on the previous paper, it is an app which uses Codex to translate informal math theorem statements into Lean. It is chat-like (before ChatGPT), so the user could instruct the model on how to correct the translation.
- Draft-Sketch-Prove. Solves competition math problems in three stages. (1) Uses Minerva (a large language model for informal math) to solve the problem in informal language. (2) Uses Codex to translate it to Isabelle/HOL, but leave the low level details empty. (3) Uses SledgeHammer to fill in low level details. (If they give it 100 attempts per problem, it has about a 35-40% success rate.)
- LeanAid. Like LeanChat, it again translates statements into Lean, but has very tight integration with Lean's internals so the LLM can use Lean specific information like type-checking and access to the Lean library.
- ProofNet. Provides a benchmark for auto-formalization with some baselines using LLMs.
- ChatGPT. ChatGPT came out after all these papers. Techniques which only were available to researchers or specialty apps are now available to everyone to play with. But it is also clear from the reviews of users, it has limited usefulness.
- Baldur. Uses Minerva to generate proofs in Isabelle/HOL and then provide editor feedback to correct the mistakes in them. Has a pretty good success rate, 47%.
- GPT-4. GPT-4 was just released (or made public, as it has been in Bing for a few weeks), and there have been some examples suggesting it might be even better for all of the above applications.
(Note: Success rates are difficult to measure and the above numbers may be higher for theorems already in the Library, since the models may have memorized the code in the library. So take these numbers with a grain of salt.)
import tactic.ringis the missing preamble, although the code still doesn't work. $\endgroup$