What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.
It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.
alt Hacker News
It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.