Is there a bounty system?

Stream: general

[Matthew Khoriaty]

I'm curious if there is a bounty system for Lean proofs. Something like "I'll pay $x to whoever sends me a Lean 'translation' of this paper," "I would like to have an optimal solution to this problem for my software," or "I'm working on a complicated proof and would like for someone else to handle this lemma." I feel like mathematics would really benefit from a way that would allow customers to "buy" proofs without having to understand them. Mathematicians would be directed to questions that are in-demand and could make more money.

[Andrew Yang]

I don't think most people are here because of monetary incentives. "I'm working on a complicated proof and would like for someone else to handle this lemma." is already happening here organically in the form of collaborations.

[Johan Commelin]

Academia has some sort of bounty system: the grant system. But it isn't very fine-grained, in the sense that a grant for a postdoc or phd should typically pay the bills for 1 - 3 years.

[Johan Commelin]

But industry players regularly have contracts with universities in which they formally agree to fund a phd project and the university agrees to devote the phd project on research for the industry player

[Bolton Bailey]

I don't know about dollars, but I have paid out 2000 fake internet points on a prediction market site for people who adopted my pull requests.

[Edward van de Meent]

i was this :small_amount: close to thinking you were talking about crypto :laughing:

[Bolton Bailey]

If anyone wanted to make crypto bounties, they're too late: They should have done so before this prediction market expired so they could make an insider trade!

[Bolton Bailey]

On that note: Is there a rust-based Lean checker? I wonder how hard it would be to make a blockchain bounty for FLT with some of the rust-based blockchain proof interfaces.

[Matthew Khoriaty]

Thanks for the information! I wrote up some ideas for how a Math Market system could work here. I would love to hear your thoughts.

@Bolton Bailey I didn't see your response in time to include it in my essay. Some of the ideas referenced in the Manifold Market were similar to mine, but I went at it from a slightly different direction (I don't trust crypto, and a crypto-based market is less likely to catch on than a non-crypto market) and explored some implications of a Math Market.

[Kevin Buzzard]

There was one of these for Coq a few years ago, and every time a proof of false was discovered all the bounties were immediately claimed; my impression was that eventually the people running it just gave up because of this.

[Jireh Loreaux]

@Matthew Khoriaty I think there are a lot of other dangers / exploits that exist in the market you describe. For instance, you take it for granted that a proof accepted by the proof assistant will be accepted by the person who offers the bounty. But there would be both legitimate and illegitimate reasons to deny the bounty. At the point, you need actual arbiters.

Moreover, you downplay the possibilities of malicious actors executing arbitrary code, but this is a very real concern.

[Jireh Loreaux]

I'm not saying something like this couldn't ever exist, but it's certainly not as simple as you seem to describe.

[Bolton Bailey]

Kevin Buzzard said:

There was one of these for Coq a few years ago, and every time a proof of false was discovered all the bounties were immediately claimed; my impression was that eventually the people running it just gave up because of this.

I'd be interested in hearing more about this and what the problems were that caused false to be provable. Do you have a link? Edit: Is this what you are referring to?

[Ilmārs Cīrulis]

There was short-lived proof market for Coq proofs long ago, which paid in bitcoins. I remember that I got 5 euros worth of bitcoins that I sent to friend.

[Ilmārs Cīrulis]

Ah, I see Kevin Buzzard posted about it. Sorry, too slow.

[Ilmārs Cīrulis]

11 years ago, wow. See this post on Reddit, for example.

[Kevin Buzzard]

Wayback machine snapshot and associated Twitter account

[Ilmārs Cīrulis]

Asking for a friend, what's good size of bounty today?
(If I wasn't so poor I would be generous bounty giver. Always getting stuck when proving something. :sweat_smile: )

[Ilmārs Cīrulis]

More seriously, I wish such bounty system existed. I would probably chip in for formal proof of FLT or something.

[Ilmārs Cīrulis]

Bounty system with option to crowd-fund.

[Kyle Miller]

The idea of bounties comes up often, but something I'm wondering is why use a system that leaves so much uncertainty to the people doing the work? If multiple people work on the same problem, only the first to submit a working solution wins, right? Is the whole idea to protect the buyers from needing to do any due diligence of actually understanding what they want to buy and to not have to evaluate potential contract workers?

[Kyle Miller]

Johan mentioned grants already for academia, which is open-ended and funds moving in a general direction, but in lots of other sorts of creative work in industry you set up a contractual relationship with the artist/designer/etc. for specific work products. You don't set up a bounty for "create all the illustrations for my book" and then get to pick and choose who will get paid for example (though doubtless people have tried).

[Bolton Bailey]

The second one seems like the answer to me. If the details of a contract-to-prove-theorems and a bounty-to-prove-theorems are the same in terms the amount of money and the specification, then the only difference left is the advantage to the buyer that they don't need to negotiate with a specific counterparty, they can just let any counterparty who finds the terms acceptable take it up.

[Bolton Bailey]

If uncertainty about a race to claim the bounty or being first is the issue, I imagine that could be solved by auctioning off the exclusive right to claim the bounty for period of time as long as the contract lasted, though maybe that has other downsides I'm not seeing.

[Mac Malone]

Kyle Miller said:

in lots of other sorts of creative work in industry you set up a contractual relationship with the artist/designer/etc. for specific work products. You don't set up a bounty for "create all the illustrations for my book" and then get to pick and choose who will get paid for example (though doubtless people have tried).

This is generally true for small indiviudal commisions. However, for larger / bulk contracts it is very common to feel out a number of designers and request samples (e.g., for a small fee) before seleciting one to actuall do primary request. It is a lot like the "exclusive right" auciton Bolton suggested. Similar auctions also occur with governemnt contracts.

[Mac Malone]

Kyle Miller As for the motivation behind a bounty system, itself, I can think of three major reasons:

• Speed. A first come,-first-paid model creates a fear of missing out, which can help motivate potential claimaints to solve the bounty quickly. However, this is, as you noted, this is one-sided advantage for the buyer.

• Security. A verified bounty system can help the buyer acquire goods from a domain they may not have the expertise to properly vet and thus help reduce the chance of being scammed (as you also suggested). For highly technical problem like verification, I do not find it suprising that indiviudals or small firms would feel (and be!) unable to vet sellers.

• Accesibility. Many potential buyers may not know many sellers or communities of sellers and/or may not have the ability or desire to build a contractural relationship with such individuals. An standardized, widely-knonw, automatic bounty system can remove these barriers to entry. StackOverflow is a great example of how a centralized system and bounties can open make much easier for broad audience to obtain code help than indiviual tutors or IT support could achive.

[Kim Morrison]

A closely related question here, with the apparent imminent arrival of AI provers, is how much compute people will be willing to pay for to get theorems (presumably software verification theorems more than mathematical theorems?) proved. One guesses that the compute budget for AlphaMath was ... profligate, but at some point in the near future this may become a live question.

[Bolton Bailey]

I think this is a very good point, because the value of a formal mathematical theorem can be hard to quantify, whereas for bugs in a software system, it seems easier to price what exactly is at risk if the theorem is found to be false. Even better could be provably-correct optimizing compilers, since it is clear there exactly what you are buying (namely an explicit number of saved compute cycles).

[Alexander Hicks]

To add to the discussion about proof markets/bounties: You could enable automated payouts for Lean proofs via smart contracts that verify SNARKs produced with https://github.com/lurk-lab/yatima (cc @John Burnham )