I have a variety of ideas that live on my computer/in Overleaf files/GitHub repos with my collaborators. I would like to predict which ideas I will actually be able to turn into research.
These don't necessarily reflect titles. Rather they reflect ideas, some of which might eventually be combined in some form with other ideas. Some of them are anonymized to avoid leaking ideas, feel free to DM if you are interested in hearing about details / betting on them for me / participating in the projects themselves.
@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.
@kiudee Anyway, sorry if this explanation is too jargony. Feel free to ask for clarification on any of this.
@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!