How did you learn lean? I’ve played the game but I still feel lost and bewildered. Did the action of proving with LLM assistance teach you the best?

I didn’t. Claude wrote all the proofs, I just validated that it was sorry-free, didn’t have any extra axioms other than mathlib and that it proved what i wanted it to prove (there’s tools for that). I did also find a actual mathematician who did a sanity check for me.