Unknowable Math Can Help Hide Secrets

Given that they can’t be proven, so it’s effectively unpredictable and “un-generatable” ?

It's only secure until someone figures it out.

There are different definitions of "zk", of "proof". Eg do "proofs" of false statements not exist, or are they just hard to find? If they exist but are hard to find, then it's often called an "argument" instead, which is the "AR" in zk-SNARKs and zk-STARKs.

One common definition of zero-knowledge protocols is that you can make an efficient simulator that makes convincing transcripts of the protocol without knowing the relevant secret (up to and including whether the statement to be proved/argued is even true). For interactive proofs, the simulator is usually supposed to output a transcript of the messages sent between the prover and the verifier, and the trick to making the simulator work is to choose later messages before earlier ones (e.g. challenges before commitments). But in non-interactive proofs, there's only one message, so that trick doesn't work and the simulator would have to output the proof itself.

The Goldreich-Oren result shows that this definition of ZK conflicts with soundness, unless the type of problem you're doing ZK proofs for was easy to begin with. IIUC this is for a simple reason: if a simulator can efficiently output a convincing proof of any true statement of the type your zk proof system covers (this is the zero-knowledge property); and if for false statements there is no proof that will convince the verifier (soundness); then you have an efficient algorithm for checking whether the statement is true or not, which is just to check whether your simulator convinces the verifier. This means that the underlying problem is by definition easy, so there's not much point to having zk proofs for it.

Goldreich-Oren doesn't apply to zk-SNARKs or zk-STARKs, because they are not perfectly sound, and in particular because you can get around the impossibility using the trusted setup in zk-SNARKs (essentially a secret key that lets you efficiently prove false statements) and/or by messing around with the random oracle model (pretend that the hash functions are replaced by magic, and then let the simulator tinker with that magic). Also zk-S?ARKs are arguments of knowledge (not just e.g. "a discrete log of this point exists" but "the prover knows the discrete log") which also changes the model.

As I understand it, the new result is basically to make your proof a NIWI-proof ("Non-Interactive Witness Indistinguishable proof", a weaker notion of zk-proof) that:

* Either [real statement you're trying to prove]

* or else [false statement that's almost impossible to prove false], e.g. "there are contradictions in your axiom system".

Such a proof can be made perfectly sound, since NIWI can be perfectly sound, and the second half is supposed to be false. There's no simulator, but if the false statement were true then there would be a simulator, where you always feed the NIWI eg a contradiction in the axiom system, instead of a proof of the real statement. (The definition of NIWI is that it should be hard to distinguish the proof resulting from these two cases.) The new paper also argues that this result, where there's no simulator but it's hard to prove that there's no simulator, is almost as good as the simulator actually existing.

Probably in practice you wouldn't do this, but you would instead try to make sure that a zk-SNARK, zk-STARK, NIWI etc is good enough in your use case.