Second Proposal for Reward Bounties

by Brown, Tuesday, October 27, 2020, 08:40 (404 days ago)

I don't like the idea of getting rid of reward bounties altogether. Since my previous proposal met with resistance, I came up with another.

There are several sets of ATP problems that came from translating from ITP libraries. Two of these are the MPTP (translated from Mizar) and the GRUNGE dataset (translated from HOL4). I managed to translate many of the problems into Megalodon's format (one step away from Proofgold's). There are 11833 problems from HOL4's library and 29586 from Mizar's library, giving a total of 41419.

If you're willing to download about 5 or 6 GB, here are two tgz files:

http://grid01.ciirc.cvut.cz/~chad/hol4_bushy_mg.tgz
http://grid01.ciirc.cvut.cz/~chad/mizar40_mg.tgz

If you want to have a quick look at a few problems without downloading them all:

http://grid01.ciirc.cvut.cz/~chad/hol4_bushy_mg/
http://grid01.ciirc.cvut.cz/~chad/mizar40_mg/

We could simply fix some or all of these 41419 as the "candidates" for reward bounties. Which one of the candidates gets the reward bounty in each block could still be randomly determined.

If we do this, I suggest sunsetting the reward bounties after some number of blocks like 45000 (about 5 years) or 90000 (about 10 years). Getting rid of reward bounties after that long is more reasonable than doing it now. After 90K blocks, each candidate will probably have two or three 25 bar bounties on them. There is a small possibility that one candidate could be chosen 32 times, leading to a deadlock condition. Some quick estimates indicate the chance of this happening is less than 1 in 10^21, so it's fair to ignore it. If it did happen, the deadlock can be resolved by orphaning a block everytime that candidate is chosen in the future, so it would not be fatal anyway.

A potential attack if candidate bounty addresses are known in advance is for someone to fill them up with 32 bounties in advance. This would make the kind of deadlock I mentioned above happen on purpose. The easiest way I can see to avoid this is to add a new condition on tx validity that noncoinstake txs cannot add bounties to those specific addresses. It's probably more efficient to disallow bounties on some "cone" of addresses that include the candidate addresses. As long as not too many addresses are in the "cone" (< 1%?) it doesn't seem too restrictive. The restriction can be lifted after block 90K (or whenever reward bounties are stopped).

Note that knowing these 41K problems in advance lets anyone work on giving proofs of them starting now. The bounties can still be placed after the theorem has been proven and can still be collected by the person that proved it in the past. The hope is that this would provide an incentive to get people proving real theorems now.

What do people think of this option?