This is fascinating to me. A couple comments and links.

Here is a course on proof theory that uses Coq [1]. It is actually the course that Vladimir Voevodsky took when he was trying to understand proof and type theory [2], [3]. While writing the midterm paper, he discovered homotopy type theory [4]. More details on the bitcoin scripting language can be found in the excellent blog post by Michael Nielsen[5].

If the escrow model is implemented, you can actually imagine the mathematical proof market maker acting like a bank, loaning out or otherwise investing bitcoins while the world waits for a verified proof; say, of the abc conjecture [6a] or the goldbach conjecture [6b]. This might be one small way to disrupt Wall St [7a], [7b]. In particular, such a market, when more highly developed, provides skilled mathematicians and scientists incentives to work on math and ( computer ) science problems in an open source format that benefits everyone - since everyone can look at and learn from their proofs - rather than quantitative trading in a closed format that actually causes long term social harm and political instability [IMHO]. I am thinking here of Goldman Sachs and Renaissance Technology founded by James Simons. Imagine if an incentive structure existed that encouraged all these smart folks to work on what is essentially verifiable open source software [8].

[1] http://www.cs.princeton.edu/courses/archive/fall09/cos441/in... [2] http://blogs.scientificamerican.com/guest-blog/2013/10/01/vo... [3] http://www.heidelberg-laureate-forum.org/event_2013/ [4] http://homotopytypetheory.org/book/ [5] http://www.michaelnielsen.org/ddi/how-the-bitcoin-protocol-a... [6a] http://www.nytimes.com/2012/09/18/science/possible-breakthro... [6b] http://xkcd.com/1310/ [7a] http://cdixon.org/2013/12/31/why-im-interested-in-bitcoin/ [7b] http://cdixon.org/2010/01/23/how-to-disrupt-wall-street/ [8] This is a pipe dream.