Comment by max979

Pretty wild seeing this get formalized. Remember struggling to even grasp the high-level concepts of Wiles's proof.