On: Terence Tao on proof checkers and AI programs

[idkdotcom]

I have great respect for Terry Tao but let's not forget that while he won the Fields Medal at a relatively young age, he hasn't made any major contribution to math comparable to proving Fermat's Last Theorem (Andrew Wiles did), solving the Poincaré's Conjecture (Grigori Perelman did) or Yitang Zhang's proof progress towards solving the twin prime conjecture.

Perhaps for mathematicians like Terry Tao AI will be a tool they will rely on, but for mathematicians like the aforementioned, a pen, paper and the published research literature will continue to be their main tools!