Post #2438871
2026-05-07 01:26 UTC
@adamshostack@infosec.exchange
Well, I guess it is in everyone's individual context that we are talking (in tao's thread). For example I am interested in acl2 rather than lean, and not pursuing llms; the last I was closely following this was the proof oriented small language model articles and philosophy of math viz proofs that are too big for humans to practically review a few years ago.
@djl@mastodon.mit.edu @tao@mathstodon.xyz @Ardubal@mastodon.xyz
Replies (1)
-
@djl@mastodon.mit.edu 2026-05-07 01:38
@screwlisp@gamerplus.org @adamshostack@infosec.exchange @tao@mathstodon.xyz @Ardubal@mastodon.xyz I'm not a mathematician, just an AI nerd from the 1970s/80s. But I don't have a problem with using computers to enumerate cases. It should be possible to _prove_ that the computer enumeration is correct without actually looking at each case. I really think that that angst is way overblown.