For the same reason that 700 vibe coded PRs, each of which 10,000 line diffs, being dumped on an open source projects is not positive for the project.
But in mathematics, there is a clear right or wrong. In coding, there really isn't.
You’re talking about whether something can be verified. I’m talking about the mental DDOS releasing work like this creates
The navier stokes paper is 166 pages long and the lean code is over 500 kloc. Nothing about that is “clear”. Someone has to real ALL of that to see if the proof is clearly right or wrong.
You can choose to ignore all the PRs, just like mathematicians can choose to ignore all the released papers.
the right may not be clear sometimes but the wrong definitely is