Post #2438868
2026-05-06 21:21 UTC
@tao@mathstodon.xyz @djl@mastodon.mit.edu @Ardubal@mastodon.xyz
I have a sort-of question about this. I guess that computer generated proofs are not new news. https://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer . Including proofs that are too large for human review to be possible or practical. On the other hand, I was surprised by the new Erdos problem 728 proof and had initially assumed that it "was really the mathematicians".
So my question - is this just more automatic theorem proving, except powered by deep learning now?
Replies (1)
-
@djl@mastodon.mit.edu 2026-05-06 22:26
@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.