🏅 Top traders

I've been working on something like this. There is a very raw version ready for messing around with.
Announcement on Lean's Zulip: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/blockchain.20theorem.20bounties/near/482741350
Repo with the contract source code and instructions how to interact with it if you're not experienced with blockchain: https://github.com/wadimiusz/lean-contract-interact

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.

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.]