LLM

Stream: new members

[Matt Chen]

Hi!
What are some LLM or Copilots with good support of Lean 4?

[Jason Rute]

That can mean a few things. Are you looking for (1) cutting edge research, (2) Lean specific user tools, or (3) something you can plug into an existing VS Code Copilot plugin/fork (like Continue or Cursor)? For (1) there is a lot of research. See #Machine Learning for Theorem Proving. For (2), try out https://github.com/cmu-l3/llmlean and https://github.com/lean-dojo/LeanCopilot and let us and the maintainers (respectively @Sean Welleck and @Kaiyu Yang) know your thoughts. For (3), the standard LLMs make a lot of mistakes with Lean (including mixing up Lean 3 and Lean 4 syntax), so your mileage may vary, but for example, recently @Kim Morrison thought that Cursor (which I think uses Sonnet 3.5) was pretty good for some Lean tasks (#general > cursor (VSCode variant with AI better than Github Copilot)).