OpenAI's new GPTs feature could help get Lean 4 Syntax

Stream: lean4

[Avi Craimer]

I've been frustrated by the fact that ChatGPT constantly gives Lean help using Lean 3 syntax even when you ask it to give Lean 4 syntax. With the new GPTs feature you can give custom instructions and upload custom knowledge.

I just uploaded the prelude and tactics from the source code with the comments removed and gave it some instructions not to use lean 3 syntax. It seems to do a lot better at generating Lean 4 syntax, although it still makes mistakes. I'm sure it could be improved further with more carefully curated code examples.

If you have a ChatGPT Plus account you can try it here:

https://chat.openai.com/g/g-3QAaNV92x-lean-4-programming-assistant

Note that I wasn't able to upload the source code directly as knowledge for the GPT, OpenAI must have a filter for detecting code files which it puts under "code interpreter" rather than general chat knowledge. I got around this limitation by putting the Lean code inside an .md file using triple backticks. This was accepted as "knowledge" for the GPT agent.