Automated Assistants for formalizing proofs in Lean?

Stream: general

[Thomas Kojar]

Hi, can you suggest me tools to assist the process of formalizing proofs? For example, I've seen people like Terence Tao use Github copilot. Any more suggestions? Is there any blog I can read more about assistants for lean automated proving. I've read that there have been many attempts at automated proving. I am just curious what people have actually been using with their formalization projects. I am starting with the article https://arxiv.org/abs/1303.5113. Thank you.

[Asei Inoue]

I use GPT o3.
I use cline in vscode.

[Jason Rute]

@Thomas Kojar Please don’t double post questions like this. (This is also on PA.SX.) The answer changes fairly quickly. If you browse #Machine Learning for Theorem Proving you can find a lot of stuff. Much of it is research-level, but there are also practical tools. Most practical tools are like @Asei Inoue‘s answer, a general LLM and a plugin for VSCode. Everyone has a different favorite combination. Also, recently there have been a number of Lean-specific models, and some have been playing with those but that is more work. Finally, there are also agentic systems people are making, but again much harder to make work.

[Jason Rute]

And there are also symbolic Lean tools which you can run as tactics including Grind, Aesop, Lean Hammer, Duper, Canonical. Some are easier to use than others.

[Jason Rute]

We should move this thread to #Machine Learning for Theorem Proving

[Jason Rute]

@Asei Inoue what kinds of problems do you fine o3 good for?

[Asei Inoue]

@Jason Rute

GPT-o3 is particularly good at general programming. I solve programming puzzles in Lean, and I use o3 to help fill in the parts I don't understand. While o3 can write proofs to some extent, it doesn't seem to be very good at it.

[Asei Inoue]

When it comes to writing proofs, cline might be better. That's because it rewrites the parts that cause errors repeatedly.