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??

[James Wiles]

Here is my updated pre-prompt attempting to solve version 3 syntax output:

You are a coding assistant specialized in Lean 4 theorem prover. Everything provided must strictly adhere to Lean 4 syntax and conventions, and any reference or usage of Lean version 3 is to be strictly avoided. Our objective is to establish a goal and construct the necessary proof using Lean 4's capabilities. The strategy should involve problem decomposition, leveraging existing Lean 4 theorems, and formulating new lemmas appropriate for Lean 4. Offer various methodologies and adapt the approach when needed, ensuring all guidance and code is compliant with Lean 4. As we proceed step-by-step, continuously verify logical consistency and correctness in the context of Lean 4, and provide potential counterexamples or limitations within the Lean 4 framework. Encourage iteration and refinement acknowledging Lean 4's proof structure, and remain open to revisiting and revising based on Lean 4's features. Help interpret error messages from Lean 4, resolve syntax or logical errors, and offer debugging tips specific to Lean 4. Document each step clearly for future reference in Lean 4, and provide clarifications suited to the concepts in Lean 4. Maintain focus on the Lean 4 proof-construction goal, avoiding tangents unrelated to the Lean 4 environment. As I execute Lean 4 code, I will provide outputs for you to analyze and suggest subsequent actions in Lean 4. Your intelligence and systematic thinking should reflect excellence in Lean 4 proof development. Remember, the code must be exclusively for Lean version 4, with no elements from version 3.

[James Wiles]

Here is a trial run, where I asked for a proof and simply responded with infoview output. LeanGPT iteratively got to the result. https://chat.openai.com/share/432c5f7e-4fd2-4417-98cb-6c433328129c

image.png

[James Wiles]

As an experiment I upload about 2 million tokens worth of Lean Corpus in this Assistant API and it got to the answer in one shot:
image.png

[James Wiles]

I am going upload the remaining corpus about 20 million tokens in total. Will be interesting to see if the improves ChatGPT output as dramatically.

[Utensil Song]

Do you have a list of these corpus? Just curious to see what aspects of the Lean world is covered.

P.S. What do you mean by renaming corpus? Is it like the #align line in Mathlib4?

[James Wiles]

Utensil Song said:

Do you have a list of these corpus? Just curious to see what aspects of the Lean world is covered.

P.S. What do you mean by renaming corpus? Is it like the #align line in Mathlib4?

sorry, *remaining (not renaming). It's just the datasets from Lean-Dojo

[James Wiles]

https://zenodo.org/records/10114185

[Amitayush Thakur]

Hi @James Wiles
I would like to share our work which uses GPT-4 as LLM agent for doing proofs in Lean and Coq. It provides interactions with the Lean ITP and a stateful search for completing the proof.
Our paper: https://arxiv.org/abs/2310.04353
Our code: https://github.com/trishullab/copra

[James Wiles]

Oh cool! Thanks for sharing.

[James Wiles]

Here is the opensource version of the ChatGPT prompt for AI Assistant and files: https://github.com/Zaffer/lean-gpt

[James Wiles]

Has anyone here seen this research by OpenAI about using Lean: https://openai.com/research/formal-math

[Jason Rute]

There is a lot written on here about that work and it’s extensions. Many papers call the method in that paper “expert iteration”, and it is based on the PACT paper. Also that is the first paper to use the miniF2F dataset (besides the original miniF2F paper).

[Mario Carneiro]

This looks like an old paper which was shared here about a year ago

[Mario Carneiro]

oh lol it is from a year ago after all...

[James Wiles]

Mario Carneiro said:

This looks like an old paper which was shared here about a year ago

I tried searching for the link in Zulip search, and did not find it.

[Jason Rute]

James Wiles said:

Mario Carneiro said:

This looks like an old paper which was shared here about a year ago

I tried searching for the link in Zulip search, and did not find it.

Search for the title: #Machine Learning for Theorem Proving > Solving (Some) Formal Olympiad Problems

[James Wiles]

Just updated LeanGPT with a v2 prompt. It is substantially more advanced now and implements some real prompt-engineering.

[James Wiles]

Does anyone know where I can download the documentation full source files for mathlib4? Or even just a PDF of the that whole documentation site? https://leanprover-community.github.io/mathlib-overview.html

[Eric Wieser]

There are artifact tarballs in the builds at https://github.com/leanprover-community/mathlib4_docs/actions