4 ms·
It's a proof, but not a formal one. It doesn't define the notion of "program", for example. It's somewhere between an informal proof and a proof sketch (a corre
by pw0ncakes 16y ago
It's a proof, but not a formal one. It doesn't define the notion of "program", for example. It's somewhere between an informal proof and a proof sketch (a correct and valid one, of course).
A formal proof is a sequence of statements where each is either an axiom or derived from previous ones via a set of derivation rules, and wherein assessing the validity of each axiom statement or derivation can be done "typographically" (mechanically and primitive-recursively). It's nigh-impossible to write a human-readable formal proof of anything interesting; the vast majority of mathematical papers published are informal proofs.
(Of course, this diversion doesn't detract from the matter of this proof-poem being very cool.)
- ryanjmo 16y agoYes I am sorry, I believe I ment "it is in some ways a formal proof." It is indeed a proof sketch. With a preliminary section defining things more rigorously, I do believe that this is publishable in most of the Cryptography conferences I have published in.
- alain94040 16y agoWith a preliminary section defining things more rigorously I do believe that this is publishable in a conference on Cryptography [trying to get the rhyme going for you]
- kaddar 16y agoActually, that gives me a sort of unique idea: An online, wikipedia like proof database with understandable informal proofs with click-to-expand (inline) annotated sections, if you click them, they would expand into proof of less formal claims. The idea would be that we generally share understanding of obvious axioms (and thus, allow them to be request-able assumptions), and so can enhance readability.
- chbarts 16y agohttp://us.metamath.org/ http://us.metamath.org/ Do you know about Metamath yet? It's something similar to what you want, but it's all in a single program as opposed to being web-based.