Hacker News Reader

Comment by Tanjreeve | Hacker News Reader

The point isn't that 1 person can understand an entire smartphone silicon up. It's that 100% of a smartphone can be understood by people. A maths theorem that can only be partially understood/proven only has value as marketing collateral.

View on HN

>A maths theorem that can only be partially understood/proven only has value as marketing collateral.

There are many problems that aren't "interesting" in a mathematical sense but can still have valuable proofs. The entire field of formal methods in software development is mostly about this kind of problem. If I want to be sure that no input can cause out-of-bounds memory access, or that my superoptimizer found the lowest possible cycle count, I don't care if it's elegant, I just need some machine-readable proof I can run through my trusted verifier.

When we use verification to build software. We have an actual software as an output and hopefully some sort of problem solvsd the verification is also not in an of itself valuable.

The verification itself is valuable because it gives us confidence that the software is correct. This knowledge changes what we do with the software. E.g. do we need to sandbox it before processing untrusted inputs? Is it safe to put it on a hostile network? Can we use it to control an airplane or a nuclear reactor? Even if the code remains identical, formally verifying software improves it because it lets us use it in situations where unverified software would be too risky.

For one person that understands a proof of some matrix multiplication algorithm lowering its current complexity bound in an useful way (e.g. not with absurdly gigantic <= 2nd order polynomial term), there's likely thousands of companies willing to pay for the improved efficiency

And if anything that useful does come out of this output/"slop dump" then that might begin to make a strong argument for it. But every other time it was "that's the theorem done for the headline figuring out everything important and how to use it is an exercise for the reader".

> A maths theorem that can only be partially understood/proven only has value as marketing collateral.

If this is true, then what's really the point of math? A lot of math is actually useful. A proof regarding cryptography, for example, would have practical application even if not understandable by humans.

Cryptography is 100% understandable by humans so I'm not sure what the point is. You do understand that the argument isn't everything has to be understandable by every human right just to check?

Reply on news.ycombinator.com