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.