What tool do you use to apply LLMs for Lean?

Stream: Machine Learning for Theorem Proving

[Mario Xerxes Castelán Castro 🇲🇽]

I have seen @Kim Morrison mention Claude multiple times. What software do you use to interact with it? I am interested in the answer from anybody that uses LLMs and Lean.

[Nehal Patel]

Hi Mario, I use claude code and codex -- I've started writing a blog post about some of my experiments here: https://g-research-innovation.github.io/lean4-llm/blog3_three_horsemen (still a rough draft / WIP)