Post #2438859

2026-04-29 04:54 UTC

@androcat@toot.cat Thanks for the response! I think there's still two counterarguments: 1. For informal proofs, RL prioritizes reasoning that appears valid, and I'm not sure how much they use things like known results 2. Tools like Lean both give feedback on valid proofs enabling systems to learn to produce them, and drastically reduce the checking surface (down to just the definitions).

Replies (1)

@androcat@toot.cat 2026-04-29 05:03

@jac@types.pl If we're going "this tool doesn't know how, but if we add this other tool that also doesn't know how..." then we know how that works out. It won't end up magically fixing the issues. There are some well-proven obstacles to actually defining solution-space for crawling. But GenAI is not even crawling solution-space. They are literally just rehashing past mathy text to produce the appearance of proofs. A text with "the appearance of a proof" is still not likely to actually be a proof, because math is not about arguing in a familiar-sounding manner, it's about fitting together known bits of math (bits that provably are valid in combination, at that) to get from a common starting point to the particular destination, either building up the particular statement to be proven, or locking down its environment to the point where it is apparent that it holds for some given range.

Open ##2438860