I asked him more than 10 years ago if he would be interested in a formalisation of the proof, and he politely declined. I guess he was right to decline, my proposal would not have been viable then anyway.
Yeah, I was wondering how can debates like these exist nowadays when formal methods appear to my layman's eyes as the ultimate arbitrer of proof. Is that not how the math community looks at it?
