3 ms·
You're commenting on a thread about an interview where an actual Fields medalist explains how proof assistants are actually used to do meaningful mathematical w
by g15jv2dp 2y ago
You're commenting on a thread about an interview where an actual Fields medalist explains how proof assistants are actually used to do meaningful mathematical work, today. The issues you raise are all discussed in the interview.
- qsort 2y agopractical = 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 2y ago> 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?
- PartiallyTyped 2y agoThey = LLMs. As I’ve interpreted it, they mean that LLMs and similar tech isn’t particularly helpful to theorem provers at the moment.