Will there be smart contract bounties for formalized mathematics on a blockchain before May 2024
May 2
This market resolves YES if there is some public blockchain smart contract or contracts offering at least a 100USD equivalent in bounties for formalized proofs of mathematical theorems by the market close date. A few stipulations: * The blockchain in question has to be permissionless - it should be possible for an individual with the formalized proof in hand to obtain the bounty without going through any KYC process (excluding, possibly, the process of obtaining some cryptocurrency to pay a transaction fee). * For the purposes of this question, a smart contract running on a "Layer 2" platform such as a rollup counts as a smart contract. * The proof doesn't necessarily have to be extractable from the transaction - For example, if the contract accepts a SNARKed proof of the existence of a formal proof, that counts. * The theorems for which the bounties are offered must be intentional. One might perversely define any bug in any smart contract to be a bounty for a proof of the bug expressed as an exploit - that doesn't count. * Moreover theorems must be "mathematical". One could imagine an intentionally-made bug bounty for a program with a smart contract that rewards a proof of an exploit, but that wouldn't count: This focuses more on formalizations of problems which are more explicitly mathematical. Examples might include: * Open problems such as P vs NP, or the Riemann Hypothesis. * Resolved-but-complicated theorems such as FLT. * Easier mathematical theorems such as the infinitude of primes. * Blurring the line for the above might be a bounty for a proof-of-correctness for some cryptographic scheme which relies heavily on mathematical concepts. In this case, I'd probably use my best judgement, but as a rule of thumb, I would say that if the theorem can be found in the literature somewhere, it's probably mathematical enough.
Get Ṁ200 play money
Sort by:

I've been wanting to make some sort of a public canonical ¹ theorem-proof-bounty thing for a while. Maybe you (or someone) wanna jump in on this?

¹ in the sense of having a united knowledge aggregation system

@wadimiusz It's a cool thought, but hard to make work. You might be interested in this project some guy posted on the Lean forum a while back.

@BoltonBailey This marketplace of theorems is very much in the vein of the kind of thing I'm thinking about, but they seem to approve submitted proofs manually, unless I'm missing something?

There's a whole bunch of stuff that's unblocked by accepting / rejecting the submitted proofs automatically. You'd basically get the equivalent of bitcoin mining for theorems, where participants try to invent better ways to generate proof candidates until some proof candidate "clicks". And there's already a whole toolset (like Lean) for verifying proofs, so why not use that?

That's another reason I was interested in your description of smart-contract proof bounties.

Also related: Section 5.2 of this paper. They seem to be saying that this is possible with their system, but I'm not sure if they have actually done this.

Related to the economic workability of this idea.

bought Ṁ1 of NO

I bet only 1 mana on No, because that would be a lot of efforts to solve a problem that doesn't exist.

However, more stupid things have been done in the crypto area. I find my predictions wrong too often by assuming people won't do something that will not work.

@Zardoru You may have problems with blockchain (I do some), but how exactly this is a problem that doesn’t exist? (It can be stated without blockchain in mind, so the blockchain one is an option which at least needs to be argumented out separately.) Contemporary mathematics, as well as science, do have problems in that vein. Always had, but only now do they gain more and more importance because humanity is becoming in a sense too big and too fast, and the corpus of collected data too vast. There are orientation problems, logistics problems, reproducibility problems. Formalized maths and a market-like thing for proofs or reproducibility are gaining importance, no matter if anybody likes it or not.

[I might be too vague and formulaic but I just needed to at least somewhat reduce potential misinformedness and my friend wouldn’t be going to write themselves so here we go, I wrote as best as I could with the time at hand.]

More related questions