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.