“There’s a perception of mobster behavior” from leading AI companies, one mathematician tells WIRED as OpenAI prepares to release more than 100 new solutions to unsolved problems.
Hmm, how would you picture that working? It says a system of axioms can’t prove itself consistent. I have no idea what axioms they used for this technically-a-proof, but it seems likely it’s something pretty standard, where an inconsistency would be even more world-shaking than “a Clay problem was solved”.
Also I wonder why I even trust lean as much, havent even read its code.
The Curry-Howard correspondence is pretty mathematical, so there’s at the very least a tendency to trust it as much as, I dunno, modular arithmetic.
Maybe the implementation of the basic type-checking could be buggy, but just like every other small and well-used software library (think C stdlib, or something), you should generally look at every other possibility first. If you accept the typing is correct, then the whole proof and whatever add-ons used must also be correct.
Hmm, how would you picture that working? It says a system of axioms can’t prove itself consistent. I have no idea what axioms they used for this technically-a-proof, but it seems likely it’s something pretty standard, where an inconsistency would be even more world-shaking than “a Clay problem was solved”.
The Curry-Howard correspondence is pretty mathematical, so there’s at the very least a tendency to trust it as much as, I dunno, modular arithmetic.
Maybe the implementation of the basic type-checking could be buggy, but just like every other small and well-used software library (think C stdlib, or something), you should generally look at every other possibility first. If you accept the typing is correct, then the whole proof and whatever add-ons used must also be correct.