An automatic theorem proving project
I apologise ahead for posting something in response to this which is technically off topic, and unfortunately also mentions blockchains. The comment by &#x27;yaseer&#x27; reminded me of a vaguely related idea, so I figured some people reading this might be interested...<p>What if instead of a <i>chain-of-proofs-of work</i>, there would be a <i>chain-of-proofs</i>?<p>And, what if instead of a chain, it was a <i>directed-acyclic-graph-of -proofs?</i><p>(From now on I will use the term blockgraph instead of blockchain to disambiguate.)<p>Lastly: instead of a giant Ponzi scheme of useless deflationary pretend money, what if the blockgraph was simply backed by real dollars used to reward useful proofs?<p>That last bit is the most important: What&#x27;s a useful proof? Why would anyone pay money for such a thing? Why would anyone care about a not-a-blockchain that won&#x27;t make anyone super rich?<p>I like to imagine a &quot;superoptimising compiler&quot; that has a $1K&#x2F;annum license. That&#x27;s peanuts to a FAANG or even a medium-to-large org with a development team. This money would go &quot;into the blockgraph&quot;[1], compensating the authors of the &quot;most useful proofs of more optimal code sequences&quot;.<p>Obviously a lot of effort would have to go into designing the blockgraph to avoid it being gamed or abused, because it is a lot more complex than comparatively trivial proof-of-work linear chains like Bitcoin.<p>The idea is that each proof published to the blockgraph would be identified by its hash, and would build upon existing proofs in the chain by referencing their hash codes in turn. So each proof would be a series of terms, most of which would be cross-references, as well as some novel steps that are difficult to generate but trivial to verify.<p>To disincentivise users spamming true but useless proofs such as &quot;1+1=2&quot; and &quot;2+2=4&quot;, the system would have to penalise proofs based on the data volume of their novel component <i>plus</i> some smaller penalty of the <i>total</i> number of references, <i>plus</i> an even smaller penalty for <i>indirect</i> (transitive) references.<p>Existing proofs that are referenced get a &quot;cut&quot; of the real money income granted to proofs that reference them. This makes single-use proofs worthless to publish, and widely usable proofs potentially hugely lucrative.<p>Publishing shortcuts in the proof graph are rewarded, because then other proofs can be made shorter in turn, making them more profitable than longer proofs.<p>Etc...<p>In general, the design goal of the whole system is to have a <i>strong incentive</i> to publish short, efficient proofs that reuse the existing blockgraph as much as possible and can in turn be reused by as many other users as possible. This makes the data volume small, and proofs efficient to verify.<p>The people putting up real money can get their &quot;problems solved&quot; automatically via a huge marketplace of various proofs systems[2] interacting and enhancing each other.<p>Want a short bit of code optimised to death? Put the &quot;problem&quot; up on the blockgraph for $5 and some system will try to automatically find the optimal sequence of assembly instructions that <i>provably</i> results in the same outcome but in less CPU time.<p>A compiler could even do this submission for you automatically. Feed in $1K of &quot;optimisation coins&quot; and have it put up $50 every time there&#x27;s a major release planned.<p>Want to optimise factory production scheduling with fiendishly complex constraints? Put up $10K on the blockgraph! If it gets solved, it&#x27;s solved. If not... you don&#x27;t lose your money.<p>Etc...<p>[1] The obvious way to do this would be to link the blockgraph to an existing chain like Bitcoin or Ethereum, but it could also be simply a private company that pays out the rewards to ordinary bank accounts based on the current blockgraph status.<p>[2] Don&#x27;t assume computers! This isn&#x27;t about rooms full of GPUs burning coal to generate useless hash codes. A flesh and blood human could meaningfully and profitably contribute to the blockgraph. A particularly clever shortcut through the proof space could be worth millions, but would never be found by automated systems.