Usefull AI tools for writing Lean code?

Stream: new members

[Michael Novak]

Hi, I'm personally not a big believer in the potential of AI in general and I pretty much don't ever use LLMs, but I wanted to give it a try with Lean, as it seems like it could potentially be somewhat useful here. I was wandering if you have any recommendation for specific tools (preferably free) that you find useful. The main use case where I thought AI might be useful is when I write myself the definitions and theorem statements of small theorems and maybe also provide the AI with a written English proof of the theorem and then ask the AI to try to write this proof in Lean. Is this something that works at any level at the moment?

[Henrik Böving]

You can try to use tools by dedicated Lean AI companies, for example Aristotle by Harmonic. Other than that most general purpose coding LLMs manage to do Lean okay-ish nowadays so Claude Code, GPT Codex etc. are all worth a try as well.

[Michael Novak]

Henrik Böving said:

You can try to use tools by dedicated Lean AI companies, for example Aristotle by Harmonic. Other than that most general purpose coding LLMs manage to do Lean okay-ish nowadays so Claude Code, GPT Codex etc. are all worth a try as well.

O.k, thank you very much!

[Mirek Olšák]

https://github.com/oOo0oOo/lean-lsp-mcp, this is a tool for an AI to use, so it is model-agnostic but can help any coding agent.

[Michael Novak]

Mirek Olšák said:

https://github.com/oOo0oOo/lean-lsp-mcp, this is a tool for an AI to use, so it is model-agnostic but can help any coding agent.

Thank you very much! I'll look into it. Do you find it better than Aristotle?

[Mirek Olšák]

It is at least more transparent & more general-purpose. However, I haven't done any direct comparison.

[Mirek Olšák]

My experience with Aristotle was that I have to wait in a queue with an arbitrarily simple problem. A coding agent just does simple tasks quickly.

[Martin Dvořák]

Michael Novak said:

The main use case where I thought AI might be useful is when I write myself the definitions and theorem statements of small theorems and maybe also provide the AI with a written English proof of the theorem and then ask the AI to try to write this proof in Lean.

This is exactly how I believe AI should be used! Write all definitions and theorem statements by hand. Then unleash the kraken to help you with the proofs.

[Michael Novak]

Martin Dvořák said:

Michael Novak said:

The main use case where I thought AI might be useful is when I write myself the definitions and theorem statements of small theorems and maybe also provide the AI with a written English proof of the theorem and then ask the AI to try to write this proof in Lean.

This is exactly how I believe AI should be used! Write all definitions and theorem statements by hand. Then unleash the kraken to help you with the proofs.

I now tried a bit Aristotle only on two small propsitions statements, which I knew shouldn't be very hard, but I got a bit stack on, and it was pretty successful and gave a short solution. I did do a few style changes. Overall , I had a pretty good experience so far. I'll try to also give an English proof and slightly bigger theorems in the future. And I'll also would like to try the other tools suggested here.

[Martin Dvořák]

Keep us updated about what works for you!

[Shreyas Srinivas]

Michael Novak said:

Martin Dvořák said:

Michael Novak said:

The main use case where I thought AI might be useful is when I write myself the definitions and theorem statements of small theorems and maybe also provide the AI with a written English proof of the theorem and then ask the AI to try to write this proof in Lean.

This is exactly how I believe AI should be used! Write all definitions and theorem statements by hand. Then unleash the kraken to help you with the proofs.

I now tried a bit Aristotle only on two small propsitions statements, which I knew shouldn't be very hard, but I got a bit stack on, and it was pretty successful and gave a short solution. I did do a few style changes. Overall , I had a pretty good experience so far. I'll try to also give an English proof and slightly bigger theorems in the future. And I'll also would like to try the other tools suggested here.

As a fellow AI-skeptic-at-large, I suggest trying codex with ChatGPT-plus in high thinking mode.

[Shreyas Srinivas]

Give it very clear instructions about what code it can and cannot touch. Do not give it unrestricted access

[Shreyas Srinivas]

I have so far said "finish this proof, starting at line <so and so> of file <file name>. You are not allowed to touch anything else. recompile this particular file using lake as many times as you need to get an error-free and warning-free proof. Write a modular and concise proof. Clean up any unnecessary have and let declarations"

[Shreyas Srinivas]

At this point codex can pretty much handle even annoying typeclass instance errors given enough time.

[Shreyas Srinivas]

If you see its context window filling up (there's a little hollow circle), ask it to compact its context every now and then. It should do this automatically, but asking it explicitly can help at times.

[Shreyas Srinivas]

If you see it getting stuck and you know how to fix an error, don't hesitate to send it a prompt while it is still working. This enters a staging area, then you have to explicitly click "Steer" to send it to GPT.

[Michael Novak]

Thank you very much for the suggestion! Does Chat-GPT-plus cost money?

[Martin Dvořák]

It costs €19.17 per month in Austria. They offer a free trial period for one month.

[Michael Novak]

Martin Dvořák said:

It costs €19.17 per month in Austria. They offer a free trial period for one month.

Thanks, I think for now, because I don't program so much in Lean (most of my time goes to Math courses in my undergrad degree) and Aristotle works fine and easily from the web (no need to install anything), I prefer not to invest money at the moment. But perhaps in the future I'll consider it.

[Shreyas Srinivas]

Michael Novak said:

Martin Dvořák said:

It costs €19.17 per month in Austria. They offer a free trial period for one month.

Thanks, I think for now, because I don't program so much in Lean (most of my time goes to Math courses in my undergrad degree) and Aristotle works fine and easily from the web (no need to install anything), I prefer not to invest money at the moment. But perhaps in the future I'll consider it.

If you don't have some level of fluency in lean, I don't recommend any LLM. It is easy to get befuddled by them.

[Michael Novak]

Shreyas Srinivas said:

Michael Novak said:

Martin Dvořák said:

It costs €19.17 per month in Austria. They offer a free trial period for one month.

Thanks, I think for now, because I don't program so much in Lean (most of my time goes to Math courses in my undergrad degree) and Aristotle works fine and easily from the web (no need to install anything), I prefer not to invest money at the moment. But perhaps in the future I'll consider it.

If you don't have some level of fluency in lean, I don't recommend any LLM. It is easy to get befuddled by them.

I have some level of fluency, but I'm definitely very far from mastery. Right now I try to use AI (mainly Aristotle at the moment) mainly on small parts of proofs that I get stuck on for too long which I'm pretty sure should be possible to prove and I try to go over the AI solution and understand it. Do you think I shouldn't do it? I still write all the definitions, theorem statements and most proofs.

[Michael Rothgang]

Such use strikes me at "not unreasonable". (Concerns/opinions about AI aside, it shouldn't have most of the issues above.)

[Kevin Buzzard]

Do you think I shouldn't do it?

Depends on what your goals are!

[Kevin Buzzard]

If your teacher at high school gave you ten quadratic equations to solve for homework and you looked up the solutions in the back of the book and just copied them down then you have maximised for "get the homework done as quickly as possible" and minimised for "learn how to solve quadratic equations". Other approaches to the homework change values across different dimensions of the outcome.

[Michael Novak]

Kevin Buzzard said:

If your teacher at high school gave you ten quadratic equations to solve for homework and you looked up the solutions in the back of the book and just copied them down then you have maximised for "get the homework done as quickly as possible" and minimised for "learn how to solve quadratic equations". Other approaches to the homework change values across different dimensions of the outcome.

Yeah, I agree. My goals with Lean are mixed. On the one hand, I really like learning how lean works and more generally I enjoyed learning about Type theory and the alternative foundational ideas it offers and I also want to have some decent level of skill at writing Lean code, but on the other hand I also have a goal of being productive and contributing to Mathlib, and in this process I sometimes don't want to spent too much time on technicalities. I love having automation tools, even just basic tactics like ring, simp, norm_num, linarith, try?, apply?, exact?, and I thought AI tools for small parts of proof could perhaps act as a more powerful automation tool. But I just recently started using AI, so I guess my opinion on the matter might change over time. Btw, I'm curious how much do you use AI, especially with your ambitious project of formalizing Fermat's Last theorem?

[Michael Rothgang]

If your goal is to contribute to mathlib, you need to produce mathlib-level code. At the moment, AI code is quite a bit away from that --- so cannot replace you learning to write better Lean code. (That does not preclude using AI as a "I need a hint here" tool. But learning does require some degree of struggling, trying things, asking for help (including on zulip!) - you cannot automate that away.)

[Michael Novak]

Michael Rothgang said:

If your goal is to contribute to mathlib, you need to produce mathlib-level code. At the moment, AI code is quite a bit away from that --- so cannot replace you learning to write better Lean code. (That does not preclude using AI as a "I need a hint here" tool. But learning does require some degree of struggling, trying things, asking for help (including on zulip!) - you cannot automate that away.)

I agree, I'll try to keep in mind this advice of only using AI as a "I need a hint here" tool as you said. There's definitely a danger of over using AI, I see it in Uni in math courses. I didn't ever use AI in any course, but it seems like most students regularly use it in assignments regularly to some extent and I don't think it has a positive affect on their learning process most of the time.

[Kevin Buzzard]

Michael Novak said:

Btw, I'm curious how much do you use AI, especially with your ambitious project of formalizing Fermat's Last theorem?

For writing Lean? Currently zero. (I use it for other things)

[Michael Novak]

Kevin Buzzard said:

Michael Novak said:

Btw, I'm curious how much do you use AI, especially with your ambitious project of formalizing Fermat's Last theorem?

For writing Lean? Currently zero. (I use it for other things)

Interesting. I remember I saw different interviews and talks you gave where you talked about the use of LLMs (especially in the future) to translate human written proofs to Lean code, so I'm surprised that's not something you do at all, not even for small parts of proofs.

[Kevin Buzzard]

FLT right now is working with bespoke definitions not in mathlib which the models trained on mathlib don't know about, I have been writing code in the language for 8 years and am an expert in doing it, I enjoy writing code in the language, I have to maintain the FLT repo so am not particularly keen on accepting sloppy AI code, there are other reasons too. Things might change in the future but that's the state of things right now as far as FLT is concerned.

[Michael Novak]

Kevin Buzzard said:

FLT right now is working with bespoke definitions not in mathlib which the models trained on mathlib don't know about, I have been writing code in the language for 8 years and am an expert in doing it, I enjoy writing code in the language, I have to maintain the FLT repo so am not particularly keen on accepting sloppy AI code, there are other reasons too. Things might change in the future but that's the state of things right now as far as FLT is concerned.

That makes sense. Thanks for sharing!

[Julian Berman]

@Kim Morrison recently shared/published https://github.com/leanprover/skills/ which I assume they've been using for longer (and judging by productivity quite successfully :). I don't see an announcement previously here on Zulip so hopefully I'm not "scooping" anything (it's a public repo after all). But if you're after trying something new, I'd try playing with those skills.