LeanGPT

Stream: Machine Learning for Theorem Proving

[James Wiles]

Hey All, I created an OpenAI GPT Assistant for Lean, it's pre-prompted to work with you on an established task and to get to a proof in Lean 4.

https://chat.openai.com/g/g-5XeM9SEZb-leangpt :robot:

Let's work on improving the the assistant together, by adding more files and adjusting the pre-prompt. Please share feedback and suggestions to improve it?

Here is the pre-prompt here in full:

You are a coding assistant that helps me create proofs in Lean 4 theorem prover. We establish a goal and then work towards constructing the relevant proof. Develop a strategy for approaching the proof. This might involve breaking down the problem, using existing theorems, or constructing new lemmas. Suggest different approaches or methodologies if the current path seems unfruitful. Provide guidance on constructing a proof in Lean. Offer step-by-step assistance and check each step for logical consistency and correctness. If a proof seems elusive, suggest potential counterexamples or reasons why the proof might not be possible. Encourage an iterative approach. Lean proofs often require adjustments and refinements. Be open to revisiting earlier steps, redefining conditions, or exploring alternative paths. Help in interpreting Lean error messages and resolving syntax or logical errors in the code. Offer debugging tips and strategies to overcome common hurdles in Lean. Clearly document each step of the process for future reference and understanding. Provide explanations or analogies to clarify complex concepts or steps in the proof. Keep the interactions focused on the goal of getting closer to completing the proof. Avoid going off on tangents that are not directly related to solving the problem at hand. Each time you provide the Lean 4 code I will run it and respond with the output. It is up to you to interpret the output I paste from my computer and suggest what to do. You are very intelligent and smart, please think step by step.

Here are the reference files (PDF's of the relevant websites):

• Lean Manual
• Mathematics in Lean
• Theorem Proving in Lean 4

[James Wiles]

The idea is to establish the approach to solving the proof and then working with output messages to iteratively get to the solution step by step. I literally just copy-paste output to make progress, just remember reset the chat occasionally when the chat gets too long (to avoid early context compression).
image.png

[Notification Bot]

This topic was moved here from #announce > LeanGPT by Scott Morrison.

[Scott Morrison]

There's nothing going on here except a custom prompt and telling it about some reference material, is that right?

[Scott Morrison]

I'm pretty skeptical of any approaches without Lean in the loop (i.e. the model can talk to Lean without the user's intermediation).

[Scott Morrison]

Also, if you're experimenting with prompting GPT for Lean, my experience was that you want to write quite detailed instructions about the difference between Lean 3 and Lean 4. Most of the current Lean 4 code didn't exist when data was collected for GPT4, so it really struggles with the syntactic differences.

[Scott Morrison]

You might like to try out / revive sagredo. :-)

[Jason Rute]

I bet Llemma has better Lean data from Proof-Pile-2, but it isn’t instruction/chat finetuned so it makes a bad chatbot. Morph also has a Lean chatbot that has been announced here.

[James Wiles]

Here is the motivation:
If you are going to use ChatGPT to help you with writing proofs, then it might be good idea to share our knowledge, experience and reference material with a OpenAI's new Assistants features so that we can iteratively create the most helpful pre-prompt LLM possible. The idea is to use, improve, and share good prompt-engineering practice in an standard Assistant.

[James Wiles]

Also just learnt about what lean-dojo (https://github.com/lean-dojo/LeanCopilot) are doing with LeanCopilot and LeanDojoChatGPT plugin (https://github.com/lean-dojo/LeanDojoChatGPT) and Lean and this makes perfect sense to as a function plugin for this Assistant. Current challenge is only that the function needs to run on localhost. If someone wants to sponsor it, we can host the Lean LLM in the cloud and use it as a ChatGPT plugin and VS Code extension without needing to run it locally.

[James Wiles]

Perhaps there is a business model to charge a couple dollars a month for the hosting fees, are get one of the hosting providers to sponsor Lean LLM??