Publicly available assistants for lean

Stream: Is there code for X?

[Ryan Smith]

I've heard people mention Aristotle, Gauss, and maybe a few other ones? Which ones do people use? What is their availability for the public / how did you get access?

[Rado Kirov]

I have been wondering about this too. I use GitHub copilot in VsCode and Claude by copy / paste. I am interested in try some of these fancier tools but also not interested in super-experimental ones (should be better than copilot auto completion to be worth it)

[Rado Kirov]

Btw, most frustrating thing about Claude is how often it hallucinates mathlib theorem names.

[Aaron Liu]

I tried Copilot via VSCode but found that I usually end up accepting an autocompletion and then deleting and rewriting most of it myself, so I went back to typing up theorems by hand the old-fashioned way since Copilot wasn't really saving me any time overall

[Aaron Liu]

when I have a math question I go to AI to ask the answer and it gives me a wrong proof/counterexample and I point out a mistake and it gives me another wrong response and usually after about 10 iterations it's got something correct or I give up and try thinking on my own or asking a human or looking on mathstackexchange or something else

[Yan Yablonovskiy 🇺🇦]

Aaron Liu said:

I tried Copilot via VSCode but found that I usually end up accepting an autocompletion and then deleting and rewriting most of it myself, so I went back to typing up theorems by hand the old-fashioned way since Copilot wasn't really saving me any time overall

Just curious, do you delete it and rewrite it mostly to golf it, or is it because it isn't even close to compiling the right term correctly?

[Aaron Liu]

I don't remember

[Aaron Liu]

I think it was probably both

[Violeta Hernández]

I refuse to use Copilot out of spite

[(deleted)]

1. I just use Cursor and delete .gitignore so the agent reads mathlib. With the gpt-5 model it works well enough to make me more productive
2. No model can help you if you're weak at Lean. If you are weak at Lean, practice more

[(deleted)]

To be good at Lean conceptual understanding isn't enough you need a thoroughly rewired brain :)) AI agents are slow, you should use them when you're busy doing something else, for example eating, going out with friends, watching a movie

[(deleted)]

And you should use remote desktop so you can babysit the agent when you're on your phone

[(deleted)]

With proper use you can double your productivity

[(deleted)]

Remember to delete .gitignore and specifically tell the agent to look into the .lake folder. This is very important. And if your computer is slow get a better computer. AI agents don't like slow computers

[Kim Morrison]

Cursor's autocomplete remains way better than Copliot's.

[Kim Morrison]

With sufficiently prompting Claude code in --dangerously-skip-permissions mode can do some nontrivial things. It guesses theorem names a lot but can usually find the correct one after it reads the diagnostics and starts grepping in Mathlib.

[Kim Morrison]

I've found the chat interfaces in copilot and cursor much less capable than Claude Code. I've had occasional good results from Codex, but haven't yet tried the in-IDE version.