51% Attack via Difficulty Increase with a Small Quantum Miner

Ok, went through most of them. Now prove me wrong by publishing all my NO bets!
Out of curiosity: Do you have some ideas for mechanism design for mathlib?

@kiudee That is a particularly tricky problem. To elaborate a little bit on what my specific goal is there: I want someone to be able to put up a bounty along the lines of "$100k for a computer-checkable proof of Fermat's Last Theorem" and then have multiple people or firms contribute lemmas to the proof and eventually have the money be paid out roughly in proportion to how many critical lemmas each contributor added.

The tricky part is, if the proofs of the lemmas are freely available for all to see, there is a big incentive for the final contributor to obfuscate their proof, making it seem as if they contributed a single standalone result that did not rely on anyone else's work, and therefore leading to them getting the whole bounty. I am not sure that there is a clean solution to this problem. My best potential mitigations are:

• Making the payout depend on the size of the proof, therefore making the prover not want to obfuscate.

• Allowing a challenge period where others can submit a shorter proof, and punishing submissions that are longer proofs than they have to be.

• Making the proof of the lemmas unavailable to the public. This could be done with ZK proofs, but defeats the point: The bounty is supposed to incentivize contribution so that at the end there is a public good (namely the full proof) for the community to study and reuse.

Lol typing this out I just had an insane idea: We could witness encrypt the lemma proofs to the final full proof so that once the full proof is made and revealed to the blockchain, all the lemma proofs are revealed.

@BoltonBailey Ok WE is maybe a bit overkill, it makes more sense to use TEE or MPC.

@kiudee Anyway, sorry if this explanation is too jargony. Feel free to ask for clarification on any of this.

@BoltonBailey No harm done. As a researcher myself I want all the jargon. ;)

@kiudee 😂 There is also the entirely separate problem of just adding results on mechanism design to mathlib (revenue equivalence theorems, for example). Much more tractable!

Feel free to steal any of the ideas that don't have a collaborator, I want to see these projects done more than I want to do them myself.