Post #2438869
2026-05-06 22:26 UTC
@screwlisp@gamerplus.org @tao@mathstodon.xyz @Ardubal@mastodon.xyz
No.
The automatic theorem proving blokes were writing programs that actually tried to do mathematics. LLMs are exactly and only random text generators. Since they have a lot of math proofs in their training data, they randomly mimic math proofs quite nicely.
LLMs do not have a mechanism for checking their output. That's your job.
Lean, on the other hand, is about computer representation of proofs; building libraries of valid proof steps. Serious work. Not a joke.
Replies (1)
-
@adamshostack@infosec.exchange 2026-05-06 23:15
@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.)