Post #2438860

@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.