I wrote a post on how I dipped my toes into Lean, using LLMs to guide me.

https://interjectedfuture.com/the-best-way-to-learn-might-be...

You might find it useful. I also caveat the experience and recount some of the pitfalls, which you might enjoy as a skeptic.

Martin Klepmann seemed to like it too. https://bsky.app/profile/martin.kleppmann.com/post/3m7ugznx4...