Post #2438851
2026-04-27 15:23 UTC
Replies (5)
-
@androcat@toot.cat 2026-04-27 16:33
@tao@mathstodon.xyz The null hypothesis: Generated proofs are just stochastic mishmashings of (at best) writings in the general genre "mathematical proof". There's plenty of super-obscure (and probably unsuccessful) proof text out there to train a text-spewer on. The obscurity is the point.
-
@thilakan@mathstodon.xyz 2026-04-27 18:23
@tao@mathstodon.xyz are there any parallels in software engineering now that software generation has become abundant?
-
@Steffen@mathstodon.xyz 2026-04-28 14:53
@tao@mathstodon.xyz you mentioned earlier that for more elaborate proofs a human would still have to guide the process and provide a high level Ansatz. I imagine that the person who controls the system in such a context will already need to digest the proof to be an effective guide.
-
@novus@toot.community 2026-04-28 21:15
@tao@mathstodon.xyz Seems like a nice problem to have: too many potential proofs, and not enough trained mathematics. It may be more comfortable for us mortals to have proofs verified by humans, but that is not always possible. For example, the famous "four colour theorem" was proved by computer, and the proof then verified by computer. But (and this may be a big "but") humans wrote and checked the computer program for the "four colour theorem", whereas AI has evolved in ways mankind cannot reasonably verify.
-
@shironeko@fedi.tesaguri.club 2026-05-06 11:06
@tao@mathstodon.xyz are the "proofs" you are referring to here formal proofs? LLM generated human language proofs that no one have read sounds about as useless as bits could be.