Are you kidding/trolling? The P=NP problem is FAR more fundamental, and if proven true, would basically be a proof that e.g. public key crypto can be broken (NOT a description of how to though).
Basically, it would be a proof that all the REALLY hard (combinatorial) problems out there, have a much simpler solution, if we were able to find it.
EDIT:
NS is used daily in engineering and gas/fluid modeling. We sort of “know it works”. The smoothness proof is “just” formalizing what practitioners assume is true (very coarsely said, no intention to diminish the result!)
It’s a bit like the Collatz function IMO, empirical evidence isn’t proof, but we’ve got a huge amount of evidence for the behavior we’re trying to prove.
I believe P vs NP is a different beast entirely. We don’t even know which way the answer should go.
There is huge logistics involved in killing a handful of billion people. It would perhaps be easier for such capable AI to just steal from trillionaires and redistribute the money Robin Hood style. Could be done electronically, and likely also end world hunger.
I think we have a tendency to think first of the horrible outcomes possible, and not the more radical or even humane ones.
Please don’t misunderstand me, I value property rights as much as the next guy.
My point is that fundamental misalignment doesn’t necessarily or automatically imply max violence.
My building’s group is on FB. I’ve managed without access for over a decade.
I live a somewhat normal adult life and manage without having anything to do with Meta ¯\_(ツ)_/¯ I probably miss out on some things, but I don’t notice.
All my friends just contact me through other sources.
If you have kids, it’s more difficult - I can acknowledge that.
I would say it’s very unlikely to be the case here at least.
Of course some bugs in Lean may exist (I don’t have deep insight into Lean’s implementation and there have been bugs before), but I find it unlikely to be systematical or in a format that could affect the proof.
As I understand it, Lean is implemented in Lean and emits/compiles to C. In that C code, I’d be very surprised if any buffer overflows or stack overflows exist.
Such overflows are not difficult or expensive to detect, so if any were there, it should cause a crash instead of an incorrect result.
It’s not as in handwritten C where you can forget or omit a bounds check.
I’d say it is even less likely than seeing an overflow in the Core of Java cause an incorrect result (i.e. corruption instead of a crash) - because Lean uses the De Bruijn principle of reducing to a very small Core, that is easier to keep correct (others in this thread have expanded on this I better than I can I think).
Out of pure curiosity: Do you believe otherwise or have a reason to think I am mistaken?
Stack overflows are also trivial to check for, if one wants to. It's just comparing two pointers, plus checking for arithmetic overflow (in case the pointers run past the maximum value of the pointer type).
> A design (or implementation) cannot ever be declared “correct” on its own. It can only ever be “correct with respect to a given specification.” Whether the formal specification correctly describes the problem to be solved is a separate issue.
I live in Scandinavia, and I’m sad to say, but most progressive legislation comes from the EU.
Our national government only legislates on populist issues. Racist laws, more surveillance, less oversight of cops and authorities, bans on big dogs and burkahs etc. - either symbolic issues that affect very few people in reality or mostly just limiting freedom and civil rights, never expanding on it.
I don’t like that we have many unelected technocrats and the corruption sucks, but the EU changes my life for the better. I honestly can’t say that about our national governments over the past two decades.
Basically, it would be a proof that all the REALLY hard (combinatorial) problems out there, have a much simpler solution, if we were able to find it.
EDIT:
NS is used daily in engineering and gas/fluid modeling. We sort of “know it works”. The smoothness proof is “just” formalizing what practitioners assume is true (very coarsely said, no intention to diminish the result!)
It’s a bit like the Collatz function IMO, empirical evidence isn’t proof, but we’ve got a huge amount of evidence for the behavior we’re trying to prove.
I believe P vs NP is a different beast entirely. We don’t even know which way the answer should go.
reply