3 ms·

It would be cool to have a Patreon-like system for math proofs. But to reward solvers appropriately and at scale, the award conditions and evaluation would have

It would be cool to have a Patreon-like system for math proofs. But to reward solvers appropriately and at scale, the award conditions and evaluation would have to be very formalized and specific. This seems to be one potential, actually useful application of blockchains which support general purpose computing - if you can port a proof verifier onto them, you give anyone the ability to commit to (and claim) proof bounties. Now, precisely formalizing specific conjectures and ensuring the proof system is expressive enough but doesn't allow for the introduction of any new assumptions is another problem...

xavxav 3y ago
A blockchain provides nothing of value here, what you need is a mechanized proof, and once you have that the blockchain in no way contributes to the trust. The trust in a Coq proof comes down to "do you believe that the 8kloc kernel faithfully implements CiC+extensions and is this metatheory a sound type system?". As it is today, anyone could claim or commit a proof bounty by posting a Coq / Lean file / project online, all that's required is an email.
- 7373737373 3y ago
  Sure, any centralized group, ideally a non-profit could run it just as well, and do so without potential complications arising from computation limits. But they'd have to be entrusted with all the funds, and the financial side may be more difficult to implement. What could be a contract call would involve more real life logistics. Not to imply that the points or whatever would have to represent anything more than kudos/bragging rights. It would be interesting to see which problems have the most professional interest, say if every math PhD got 1 million points to commit.
  - lupire 3y ago
    Overhead of block chain is greater than overhead of centralization. We already have rich math guys like Simons throwing money at people doing math.
- eddtries 3y ago
  First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders?
colesantiago 3y ago
> This seems to be one potential, actually useful application of blockchain... No. Blockchain and anything crypto has absolutely no use case at all other than speculation, please stop suggesting this solution in search of a problem.
- pixel8account 3y ago
  One: anonymous[1] method of payment online. Maybe this is not a problem you like, but your statement is trivially false. [1] pseudonymous (in case of BTC) if we're being pedantic.
  - colesantiago 3y ago
    This is great use case for criminals.
cottonseed 3y ago
I actually prototyped a system like this, mostly as an exercise to learn about crypto. You can't feasibly host or verify proofs on-chain, so you need external trusted verifiers (e.g. oracles). Making sure the oracles can't front-run proof submission is a challenge. Standard formal proof system (like Lean) are sufficiently expressive, although they weren't built for this and need to be modified to make sure a proof hasn't introduced any additional axioms, as you note. The proof system also becomes a point of attack, so you'd probably want multiple, independent verifiers (which themselves have been formally proved correct). I believe these exist for some proof systems, although I'm not sure about Lean's kernel. Ultimately, I don't think this is really practical, and investing in AI proof agents is the way to go.
- 7373737373 3y ago
  > You can't feasibly host or verify proofs on-chain I came to the same conclusion with existing systems, full on-chain verification would not be economically feasible. But perhaps a special-purpose chain specifically made for this may not have the same limitations. Or Truebit-like oracle systems may be possible, where external verifiers can dispute other external verifier's assertions of correctness by running only the (potentially) wrong steps on-chain. The frontrunning may be avoided by submitting hash(accountid | secret large random number | proof) first, then once that's finalized the full proof with the random number. The random number so the proof can't be brute forced from the hash. Payouts have some reasonable delay so if someone tries to frontrun the second step by intercepting the full proof and submits both steps (possibly with a varied proof) before the second step of the first person is finalized, the first person can still prove with a reference to their first step and their working proof that they were first. This still requires some thought regarding (forced) congestion in relation to the transaction cost and bounty size. Metamath has the same problem of the system accepting new axioms anywhere, and the same $a statement being used for definitions. I have some hopes for Metamath Zero (https://github.com/digama0/mm0 https://github.com/digama0/mm0), which is a related system which may be able to fix this. I think this idea is rather synergistic with proof agents. I think more people would consider developing these if enough bounties were credibly committed. It might speed up and greatly increase the number of formalized proofs.
- 3y ago
baq 3y ago
I don't think you need the blockchain to post a verifiable, cryptographically signed proof of any theorem. A simple email is good enough for that. Blockchains are append-only databases, sometimes (usually?) with 'slow' thrown in somewhere.
- eddtries 3y ago
  First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders? That’s an app on top of the append only DB with some logic that either requires IRL groups to manage it, or a blockchain contract. I prefer the latter tbh!
byteware 3y ago
talking as someone who is building such a system, why would an avarage participant of the network give their own money, i dont think they would for the same reason i'm not running a bounty program with my dollars, the only use of having it on the blockchain is rewards without using your own money (so it's economics depends on the eventual value of the coin), for that it has to be bound to the minting process, but a purely algorithmic system for determining who gets how much based on their proofs seems elusive (think of the infinite possible proofs 1+2=3, 1+3=4...), we are going for having a central authority doing the minting for proofs (as voting based on money would hardly reflect mathematical experties)
- 7373737373 3y ago
  I'd like to personally put 5-10 bucks toward the solution of the Collatz conjecture, just for fun (and to see machine learning people grind their GPU-teeth on it). No idea about the minting process, there seems to be an infinitude of possibilities.

xavxav 3y ago

A blockchain provides nothing of value here, what you need is a mechanized proof, and once you have that the blockchain in no way contributes to the trust. The trust in a Coq proof comes down to "do you believe that the 8kloc kernel faithfully implements CiC+extensions and is this metatheory a sound type system?". As it is today, anyone could claim or commit a proof bounty by posting a Coq / Lean file / project online, all that's required is an email.

7373737373 3y ago
Sure, any centralized group, ideally a non-profit could run it just as well, and do so without potential complications arising from computation limits. But they'd have to be entrusted with all the funds, and the financial side may be more difficult to implement. What could be a contract call would involve more real life logistics. Not to imply that the points or whatever would have to represent anything more than kudos/bragging rights. It would be interesting to see which problems have the most professional interest, say if every math PhD got 1 million points to commit.
- lupire 3y ago
  Overhead of block chain is greater than overhead of centralization. We already have rich math guys like Simons throwing money at people doing math.
eddtries 3y ago
First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders?

colesantiago 3y ago

> This seems to be one potential, actually useful application of blockchain... No. Blockchain and anything crypto has absolutely no use case at all other than speculation, please stop suggesting this solution in search of a problem.

pixel8account 3y ago
One: anonymous[1] method of payment online. Maybe this is not a problem you like, but your statement is trivially false. [1] pseudonymous (in case of BTC) if we're being pedantic.
- colesantiago 3y ago
  This is great use case for criminals.

cottonseed 3y ago

I actually prototyped a system like this, mostly as an exercise to learn about crypto. You can't feasibly host or verify proofs on-chain, so you need external trusted verifiers (e.g. oracles). Making sure the oracles can't front-run proof submission is a challenge. Standard formal proof system (like Lean) are sufficiently expressive, although they weren't built for this and need to be modified to make sure a proof hasn't introduced any additional axioms, as you note. The proof system also becomes a point of attack, so you'd probably want multiple, independent verifiers (which themselves have been formally proved correct). I believe these exist for some proof systems, although I'm not sure about Lean's kernel. Ultimately, I don't think this is really practical, and investing in AI proof agents is the way to go.

7373737373 3y ago
> You can't feasibly host or verify proofs on-chain I came to the same conclusion with existing systems, full on-chain verification would not be economically feasible. But perhaps a special-purpose chain specifically made for this may not have the same limitations. Or Truebit-like oracle systems may be possible, where external verifiers can dispute other external verifier's assertions of correctness by running only the (potentially) wrong steps on-chain. The frontrunning may be avoided by submitting hash(accountid | secret large random number | proof) first, then once that's finalized the full proof with the random number. The random number so the proof can't be brute forced from the hash. Payouts have some reasonable delay so if someone tries to frontrun the second step by intercepting the full proof and submits both steps (possibly with a varied proof) before the second step of the first person is finalized, the first person can still prove with a reference to their first step and their working proof that they were first. This still requires some thought regarding (forced) congestion in relation to the transaction cost and bounty size. Metamath has the same problem of the system accepting new axioms anywhere, and the same $a statement being used for definitions. I have some hopes for Metamath Zero (https://github.com/digama0/mm0 https://github.com/digama0/mm0), which is a related system which may be able to fix this. I think this idea is rather synergistic with proof agents. I think more people would consider developing these if enough bounties were credibly committed. It might speed up and greatly increase the number of formalized proofs.
3y ago

baq 3y ago

I don't think you need the blockchain to post a verifiable, cryptographically signed proof of any theorem. A simple email is good enough for that. Blockchains are append-only databases, sometimes (usually?) with 'slow' thrown in somewhere.

eddtries 3y ago
First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders? That’s an app on top of the append only DB with some logic that either requires IRL groups to manage it, or a blockchain contract. I prefer the latter tbh!

byteware 3y ago

talking as someone who is building such a system, why would an avarage participant of the network give their own money, i dont think they would for the same reason i'm not running a bounty program with my dollars, the only use of having it on the blockchain is rewards without using your own money (so it's economics depends on the eventual value of the coin), for that it has to be bound to the minting process, but a purely algorithmic system for determining who gets how much based on their proofs seems elusive (think of the infinite possible proofs 1+2=3, 1+3=4...), we are going for having a central authority doing the minting for proofs (as voting based on money would hardly reflect mathematical experties)

7373737373 3y ago
I'd like to personally put 5-10 bucks toward the solution of the Collatz conjecture, just for fun (and to see machine learning people grind their GPU-teeth on it). No idea about the minting process, there seems to be an infinitude of possibilities.