Hacker News Reader

Comment by xavxav | Hacker News Reader

A blockchain provides nothing of value here, what you need is a mechanized proof, and once you have that the blockchain in no way contributes to the trust.

The trust in a Coq proof comes down to "do you believe that the 8kloc kernel faithfully implements CiC+extensions and is this metatheory a sound type system?". As it is today, anyone could claim or commit a proof bounty by posting a Coq / Lean file / project online, all that's required is an email.

View on HN

Sure, any centralized group, ideally a non-profit could run it just as well, and do so without potential complications arising from computation limits.

But they'd have to be entrusted with all the funds, and the financial side may be more difficult to implement. What could be a contract call would involve more real life logistics.

Not to imply that the points or whatever would have to represent anything more than kudos/bragging rights.

It would be interesting to see which problems have the most professional interest, say if every math PhD got 1 million points to commit.

Overhead of block chain is greater than overhead of centralization.

We already have rich math guys like Simons throwing money at people doing math.

First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders?

Reply on news.ycombinator.com