I just cleaned out the gutters on my house. Took a while to direct the guys I hired, but feel pretty proud of the result.
replyHow 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?
replyI 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.
reply