There are mathematical theorems of the form: “Under assumption X, these 6 conditions are equivalent. We can prove this claim by a chain of implications: 1→2→3→4→5→6→1.”. These theorems are often very non-trivial. (If they were trivial, they presumably wouldn’t be theorems but corollaries.)
Yep, and getting a solid proof of those theorems would provide insight IMO. So it isn’t what I’d call “trivial”. Though, I suppose it is possible that raising the theorem statement from entropy would require many bits of info, and finding a proof would require almost none.
[Caveat lector: I don’t know that much about this, but that’s how I see it at the moment.]
The amount of information required to find a proof of a proposition given all the information implicit in (the statement of) the proposition depends on the system doing the proof search. The system’s search order can be seen as a prior over proofs (and over potentially useful intermediate proof steps, auxiliary definitions, etc). Additional info can update the prior, so that you find the proof faster, or using fewer resources in general (or misupdate and find the proof later, or in a more costly way, or never at all).
So I think you’re right, but there are caveats.
Although it’s also possible that there’s some well-behaved class of proof-finding systems such that for any two of them, those caveats become irrelevant in the limit (of proposition/proof complexity or something?). (Logical inductors?)
There are mathematical theorems of the form: “Under assumption X, these 6 conditions are equivalent. We can prove this claim by a chain of implications: 1→2→3→4→5→6→1.”. These theorems are often very non-trivial. (If they were trivial, they presumably wouldn’t be theorems but corollaries.)
Yep, and getting a solid proof of those theorems would provide insight IMO. So it isn’t what I’d call “trivial”. Though, I suppose it is possible that raising the theorem statement from entropy would require many bits of info, and finding a proof would require almost none.
[Caveat lector: I don’t know that much about this, but that’s how I see it at the moment.]
The amount of information required to find a proof of a proposition given all the information implicit in (the statement of) the proposition depends on the system doing the proof search. The system’s search order can be seen as a prior over proofs (and over potentially useful intermediate proof steps, auxiliary definitions, etc). Additional info can update the prior, so that you find the proof faster, or using fewer resources in general (or misupdate and find the proof later, or in a more costly way, or never at all).
So I think you’re right, but there are caveats.
Although it’s also possible that there’s some well-behaved class of proof-finding systems such that for any two of them, those caveats become irrelevant in the limit (of proposition/proof complexity or something?). (Logical inductors?)