On: Terence Tao on proof checkers and AI programs

[qsort]

practical = practical for routine mathematical work, which they aren't right now, which Tao says in the article itself.

Never have I ever said or implied, here or anywhere else, that proof checkers are useless and bad and stupid.

[g15jv2dp → qsort]

> practical = practical for routine mathematical work, which they aren't right now, which Tao says in the article itself.

I see, I guess it would have been nice to be clearer from the start.

> Never have I ever said or implied, here or anywhere else, that proof checkers are useless and bad and stupid.

Did I say you did?