logoalt Hacker News

drivebyhootingtoday at 5:08 PM1 replyview on HN

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?


Replies

empath75today at 5:11 PM

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.