Lean snippets
Lean snippets
Beginning a collection of Lean snippets
For some time now, I have been working on learning Lean and thinking about how to use AI to automatically generate proofs.
As I mentioned earlier, I attended the ICERM workshop on “Autoformalization for the Working Mathematician”, which was really good.
However, when I’m working on a proof using LLMs (a combination of GPT-4 o3 and Claude), I sometimes find that I would like to see examples of how to use Lean commands and tactics.
That is why I decided to begin collecting them in my blog in the form of real micro-blogging.
I hope I can keep up with this for some time.
Enjoy Reading This Article?
Here are some more articles you might like to read next: