Post #2438870

2026-05-06 23:15 UTC

@djl@mastodon.mit.edu @screwlisp@gamerplus.org @tao@mathstodon.xyz @Ardubal@mastodon.xyz I find it pretty amusing that people are arguing what constitute good math proofs with .. checks notes... Terrence Tao. Y'all might want to read https://dl.acm.org/doi/10.1145/3750038 (or, in the same issue, https://dl.acm.org/doi/10.1145/3788649, in which Dr. Tao is quoted.)

Replies (2)

@screwlisp@gamerplus.org 2026-05-07 01:26

@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

Open ##2438871
@djl@mastodon.mit.edu 2026-05-07 01:27

@adamshostack@infosec.exchange @screwlisp@gamerplus.org @tao@mathstodon.xyz @Ardubal@mastodon.xyz I'm not arguing that LLMs cough up _bad_ proofs, I'm pointing out that they cough up _unchecked_ proofs. Whether those unchecked proofs are useful food for thought, or a cesspool of random garbage, is in the eye of the beholder. But the bottom line is that they are randomly generated proofs. Thinking that they are more than that is a category error.

Open ##2438873