Hacker News Reader

Comment by ryanjmo | Hacker News Reader

This somehow seems easier to follow than a formal proof (even though it is actually a formal proof). Fun times!

I wish my professor gave us this in my CS Theory course. Would have made it ten times as much fun, and much less dry.

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.)

Yes 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.

With 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]

Actually, 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.

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.

Reply on news.ycombinator.com