Proofcoin: A reward system for proof solving

[void4]

A system that lets anyone set bounties on conjectures and automatically rewards their proof.

Background

There are several reasons why I'm very interested in this kind of survey/system specifically:

1. It would let anyone set pseudonymous rewards on mathematical proofs.

2. Formal theorem databases are still at an undergraduate level. Appropriate incentives might help them to catch up to the cutting edge. If well known, it could also lead to more interest and development of Metamath-associated tools and understanding.

3. It's just interesting to know, from an external cultural, organizational and funding perspective which conjectures are most valued in terms of reputation and utility not just by organizations and grant-givers, but by mathematicians individually and also (globally) put together.

4. It could serve as an indicator and incentive, and perhaps point of discussion (I assume also heated debate ;) ) for mathematicians themselves.

5. It could provide a way for automated theorem proving researchers (recently, there has been a lot of progress with neural networks, using Metamath as proof system: https://twitter.com/spolu/status/1303578985276887042 (OpenAI)) to know what to do/reward them. This is where asking for solved-yet-unformalized problems would especially make sense.

Theory

What if people introduce new axioms that make everything provable?

Disable introductions of $a. But what about definitions, which also use $a?

Metamath Zero distinguishes between axioms and definitions and also avoids potential grammar ambiguities, because it uses trees instead of lists of tokens. However, the proof file spec is not fixed in stone yet.

What about unprovability?

• figure out a way to make unprovability statements <- what about unprovable unprovabilities?
• also, see reward time limits

Implementation

Since putting full proof verifiers on the Ethereum blockchain is too expensive (https://github.com/void4/notes/issues/29) (especially with the current gas prices, where verification of even compact proofs would require dozens of dollars in transaction/execution costs) there might be some merit to creating an independent (or centralized) one that already included such a program in its base layer, or as a contract on top.

I don't like the idea of "financializing" (basic) research too much, because it can set the wrong incentives. However, incentivizing people, companies to do math might be a worthwhile thing to do.

• allow transactions only through proofs?
• allow multiple proofs of the same statement? Perhaps constrained rewards: proof must be within maximum length and steps etc.
• allow the same proof?

Related projects

Gitcoin: https://gitcoin.co/explorer (+gitcoinbot https://github.com/Zilliqa/zilliqa-bounties/issues/2)

AsOne: https://asone.ai/ ResearchHub/ResearchCoin: https://www.researchhub.com/

Token Journal: https://www.youtube.com/watch?v=NW32GlSTQDs