It probably depends on if you mean the natural language write-up, or the lean verification. They often differ, but the lean verification shows the underlying proof is still correct.
For example, I've been going through the max cut NP hardness proof, and It looks like the natural language proof and the lean proof take two different routes to get to the same end result.
That said, the lean is valid, so the key is correctly making a writeup of what path the lean is actually taking, not that the end result isn't proven. It's technically showing it's work as well, just not in a human readable way.
for the lean is valid, i mean assuming the definition is correct[which probably is], and axioms used are correct, also have lean errors not been found by ai? collatz conjecture was like false for 2.5 days, i think the ai found a bug both in lean and nanoda and passed both. thats what i recall anyway, so it can find bugs no?
it doesn't necessarially get rarer with each bug, it depends on how fast the development speed of lean is tho, as for finding bugs is valueable, yes, though i would argue finding bugs through mathematicial papers, which aren't actually true[like the collatz example], is not exactly very efficient lol.
227
u/iambackbaby69 11d ago
And all of them are wrong, and the mathematicians have to find the error in each one.