1,000🏅 Top traders
| # | Name | Total profit |
|---|---|---|
| 1 | Ṁ250 | |
| 2 | Ṁ60 | |
| 3 | Ṁ53 | |
| 4 | Ṁ36 | |
| 5 | Ṁ24 |
People are also trading
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
@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.
@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.]