blockchain theorem bounties

Stream: general

[Vadim Fomin]

I’ve been working on a smart contract for theorem bounties. That is, if you want a theorem proven, you can stake money that someone could claim if they submit a correct proof. A very raw first version is starting to look ready. 

No worries if you haven’t messed around with blockchain much - I made a repo with instructions on how to interact with said smart contract without the pain of interacting with blockchain: https://github.com/wadimiusz/lean-contract-interact 

You need to be comfortable with Python, though.

It’s play money for now; you don’t need to spend any real money, and there are no regulations / tax implications. 

(Getting the play money is an annoying part in the instructions; if none of the faucets work for you, ping me and i’ll help you.)

Why am I doing this? Partly it’s just a cool thing to do, but also, I’m really curious if having theorem bounties could somehow improve the life of a Lean enthusiast (that is, when we switch from play money to real money). 

I don’t understand your workflow well enough, so I wanted to throw an early, naive version out as soon as possible, to hear if something like this could make your life easier in any way, and how it could be integrated into your workflow. Only then will I work on a nice interface - I need to understand what that would look like to be convenient for you.

I expect that, if it does prove useful, the initial use case will be something like “frustrated Lean user doesn’t know how to prove this basic lemma; on the other end, a starving grad student is grateful to have the ten dollars”. In general, the hope is not just to incentivize Lean research, or align incentives, but to create better connectivity of knowledge  - to make a place where different researcher’s pieces of knowledge meet.

How can you help? 

For one thing, please just mess around with it, try depositing theorem bounties, claiming bounties, submitting correct proofs, incorrect proofs, proofs with sorries, and then tell me if you could see any uses for it, and what they would be like.

For another thing, we really need a better oracle. (Oracle is the offchain thing that checks if a proof is valid.) I’m a complete baby at Lean; I just wrote a very basic oracle that creates a file with 

theorem simple_theorem {theorem} :=

{proof}

and runs lean theorem.lean to check the exit code (and check for sorries). This probably has vulnerabilities, and only supports very simple proofs. One would want to pass more complex theorems, proofs, and entire projects. If we make something more complex, and we can make an API out of it, I can turn it into an oracle and integrate it into a smart contract.

PS I deposited some bounties for the following theorems, just to get you started:

(n : Nat) : n * 1 = n

(P Q R : Prop) (h1 : P -> Q) (h2 : Q -> R) : P -> R

{α : Type} (l : List α) : l.reverse.reverse = l

{α : Type} : (id ∘ id : α → α) = id"}

{α β : Type} {f g : α → β} : (∀ x, f x = g x) → f = g

[Kim Morrison]

Please post a bounty for False, so that people can start pointing out the vulnerabilities in your checker. :-)

[Kim Morrison]

If you check the recent "Code with Proofs: the Arena" thread you'll see some initial hints for doing this properly.

[Vadim Fomin]

bounty for False done :)

[Jineon Baek]

I like the idea! So for now we have to trust a single machine/entity that runs the Lean oracle, right?

[Vadim Fomin]

Yes. I really dislike this, since the whole point of blockchain is minimizing trust.

The problem of trusting offchain data is not new. There are solutions for stuff like prices (like if your contract needs USD / ETH prices or whatever) - there is this thing called chainlink; it runs many nodes, and outputs and aggregated value, so that even if some nodes are malicious or unavailable, the aggregated value is still valid.
So one idea would be for many Lean enthusiasts to run Lean nodes for checking proofs (for compensation), and the oracle would aggregate the nodes' outputs in a trustless way. But then the price of using the oracle increases because we need to compensate the node operators :(

Or here's a completely unrealistic decision: we could try to port Lean into the Ethereum blockchain itself somehow. Languages like Solidity are just wrappers over low-level instructions; we could compile Lean for Ethereum Virtual Machine somehow; but this is a nightmare to get done and the cost would skyrocket.

Maybe there is some way for me to verify for you all the code that runs in the oracle node?

[Vadim Fomin]

Alternatively we could build our own consensus mechanism built on Lean proofs :) There is an idea in the web3 community called "proof of excellence". For example, there is this "primecoin" which you mine by providing sequences of prime numbers. The idea is to make mining computation something useful, instead of useless thrashing like bitcoin. This idea is kind of abandoned, and primecoin is worth like two cents now. It would be cool to build our own blockchain where to mine it, you have to provide / validate lean proofs :D

[Miguel Marco]

One possible approach is to compile a lean verifier in a SNARK system, so that you have an external verifier of the submitted lean code that generates a succint ZKP, and a (much lighter) verifier for that succint proof in the blockchain level.

[Vadim Fomin]

Yeah, that sounds like a good idea!

[Vadim Fomin]

But is it realistic to compile a lean verifier in a SNARK system? is that something you folks have been up to?

[Miguel Marco]

A verifier that checks a proof of bounded size, requiring a bounded number of steps, in principle should be doable in any universal SNARK system (another question is how big those bounds can be).

The unbounded case, that's another story. My impression(without having thought much about it) is that it could be a fit for a composable SNARK system, where you can create proofs for each small step, and combine them recursively into a final proof.

[Miguel Marco]

It would be an interesting research project in any case.

[Markus Himmel]

I don't know anything about these things, but I believe there is some progress in these directions at https://github.com/argumentcomputer/yatima

[Bolton Bailey]

Other prior work is zkPi https://eprint.iacr.org/2024/267

[Joachim Breitner]

Don't we have a wasm version of Lean? That could run on some of the wasm-based blockchains out there.

[Bolton Bailey]

Success!
https://sepolia.etherscan.io/tx/0x846b6b223e4809c4caf28b076f05b5621da212c95209bc2df97dd323efbeca66

[Bolton Bailey]

A bit weird that etherscan says that the state of my balance didn't change here, but you can definitely see I have 0.2 more testnet ETH than I had at the start of the transaction if you look here.

[Bolton Bailey]

(I did the (P Q R : Prop) (h1 : P -> Q) (h2 : Q -> R) : P -> R bounty)

[Vadim Fomin]

Yay! I can see your proof. Thank you for testing the system!!

[Vadim Fomin]

The transaction you're looking at is the one where you called my contract's method, right? It's not the transaction that brings you the money. First you trigger the method, then it sends a request to the oracle, then the oracle triggers a fulfill function in the smart contract, and only then does the contract send you your play money :)

[Vadim Fomin]

The transaction that brought you money is this

[Bolton Bailey]

Ah ok. I would still expect that transaction to show up somewhere on my page though.

[Vadim Fomin]

It's because it's listed in the "internal transactions" which is a separate tab. I'm not sure what it means anyway.

[Bolton Bailey]

If I were doing this for real, would I have to trust a sequencer not to front-run my transaction by replacing my account with theirs?

[Vadim Fomin]

Hmm, there probably is some way to steal your bounty requests... Like when you broadcast the transaction, someone could send the same transaction at the same time but with much more gas... Maybe when we graduate the system into mainnet, we would have to introduce some encryption somehow?

[Bolton Bailey]

Ok I have made a new bounty for (n : Nat) : ∃ a b c d : Nat, a * a + b * b + c * c + d * d = n here

[Vadim Fomin]

Thank you for playing around with this!!
One thing that's terribly missing now is a capacity for checking which theorems have bounties attached to them, so that anyone could see that (n : Nat) : ∃ a b c d : Nat, a * a + b * b + c * c + d * d = n has a price on its head. I'll get it done, but this should be part of the interface, not of the smart contract itself, I think (or people would have to pay gas fees for memory / storage). So I'll do this once I understand what interface lean folks prefer / how people would generally use this.

[Bolton Bailey]

The god-tier move would be to integrate it with the "Arena" project that was mentioned above (github, thread) so you can see bounties and claim them, all from a web interface.

[Bolton Bailey]

Not sure how hard that would be, I've never really heard of a framework for integrating python with a webpage.

[Vadim Fomin]

I already reached out to Arena's author @GasStationManager and we chatted about collaboration :) Hopefully we will at least collaborate on the verification part - that piece of technical challenge is straight-up identical in our projects - but it does feel like our projects have potential for interaction, at least, or maybe even unification. The visions between the projects are somewhat different (in the long run, Arena is intended for AI proving correctness of output code as an alignment thing, if I understood correctly; my fondest hope is to create better connectivity for knowledge in general), but we do play in the same sandbox, so to say.

[Vadim Fomin]

I don't think there would be any technical challenge with setting up a web page at all. If Metamask's integration is easy (so that people don't have to bother with prividing private keys etc. and they know that the private key is not sent anywhere), I could throw it together pretty quickly. I didn't do it to begin with because I wanted to understand how people want to interact with it, if there are any expectations, any points where this project would help with their work routine etc.

[Vadim Fomin]

(what does an octopus reaction mean)

[Bolton Bailey]

Octopus is for celebration

[Bolton Bailey]

Screenshot 2024-11-16 at 11.03.07 AM.png
See how happy it looks!

[Bolton Bailey]

Anyways, this is totally sick, and if it had existed in May 2024 I would definitely have deployed it on mainnet and put some ETH on a bounty for Fermat's last theorem so that I could have resolved this YES.

[Vadim Fomin]

Thanks man! I totally plan to make this a real, convenient, helpful service, and if you continue to be interested in messing around with it, your feedback will be invaluable; that's how I will know what is useful and how to make something people want. Needless to say, if you would have fun co-developing any of this, this would also be most welcome.

[Vadim Fomin]

I guess the plan for now is to:

• figure out a better oracle (probably with using withImportModules and checking that the proof has the right type),
• throw together a crappy minimalistic interface and make the interaction slightly less annoying, so that a bit more people join in with their use cases.

[Bolton Bailey]

Ok, I'm looking into the arena more and I see that much of the code is actually in Python! Let me look into it more and see if there is a straightforward way to integrate this into the web interface that that project has for submitting and claiming bounties.

[Vadim Fomin]

I think the pain point would be to integrate infura, metamask etc.
On the other hand, if we host an interface, we can just use our own infura, it should be well within the free tier.
So it's just about authorization (and helping people get play money)

[Vadim Fomin]

Asking people "please enter your API keys and your private key to your blockchain account" would look much more suspicious from a web page than inside a script - at least you can (and are encouraged to) read the script and make sure it doesn't go anywhere...
If we use something like MetaMask or WalletConnect, people will at least know we're not trying to steal their account

[Vadim Fomin]

Actually, do we even need to integrate blockchain authentication into the interface on the first steps? Maybe I could start with a UI where I trigger the requestBounty function from my own account; all people would have to do is press a button on the site and specify the address to which the bounty would be sent. It woudn't work for depositing bounties, only requesting; and it doesn't scale (definitely it's not good enough for mainnet) - if nothing else, I would have to pay the gas fees for everyone; but it would be a nice start to give people something they would play around with without all the setup hustle.

[Kyle Miller]

(Regarding the octopus, someone in the early days of Zulip discovered that if you put the octopus emoji underneath another emoji, it looks like the octopus is excitedly holding it. We haven't used it that way on this particular Zulip instance, but that's apparently why it's in the "popular" section for emojis.)

:octopus:

[Bolton Bailey]

Vadim Fomin said:

where I trigger the requestBounty function from my own account

Yes, this seems simpler. This gets around the address substitution issue. If you are worried about people making lots of bounties and running out of testnet eth, you can have people making the bounties pay for their own gas out of the funds they put in the bounty.

[Geoffrey Irving]

Kim Morrison said:

Please post a bounty for False, so that people can start pointing out the vulnerabilities in your checker. :-)

Aren’t all the bounties for False?

[Vadim Fomin]

No, what makes you say that?

[Geoffrey Irving]

Once you prove False, you get all the bounties.

[Vadim Fomin]

Yeah, I misunderstood your initial phrasing:) that’s pretty much the point — allowing an attacker to drain funds.

[Alok Singh]

Kyle Miller said:

(Regarding the octopus, someone in the early days of Zulip discovered that if you put the octopus emoji underneath another emoji, it looks like the octopus is excitedly holding it. We haven't used it that way on this particular Zulip instance, but that's apparently why it's in the "popular" section for emojis.)

:octopus:

aww

[Vadim Fomin]

@GasStationManager has been working on this really cool project called SafeVerify (github here). It will be useful to check submissions both in their Arena project and in my TheoremMarketplace thing.

So I changed the oracle and deployed another smart contract that uses SafeVerify to check submissions. The contract is deployed at 0xc671A4a18DA81D6Df1A9C3619045D10FaCFB3936. The ways to interact with the contract are the same, but the format of the submissions has changed.

Now, both the theorem and the proof should be valid lean files. Example:
theorem:

theorem zero_add (n : Nat) : 0 + n = n := sorry

proof:

theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero =>
    rfl
  | succ k ih =>
    rw [Nat.add_succ, ih]

That is, the submission should define the same things as the bounty file, but without placeholders etc.

[Vadim Fomin]

I realize this is not straightforward for people to play around with. I intend to make a site with MetaMask integration which will take away the pain of interacting with blockchain, so you will just submit the proofs right on the site and earn your honest play money :)
(And real money in the future)

[John Wargo]

I've been teaching myself Lean4 with the goal of proving properties about software and engineering standards, and I wanted to say that this is an interesting idea, because it strikes me as a next-level sort of bug bounty program (given a high enough bound on steps and size, which is at least problematic for anything worthwhile).

Instead of today's "here's my code, I'll pay you if you find problematic inputs" it becomes "here's my code and its goal, I'll pay you if you can prove (or disprove?) that there are no problematic inputs". I'll note that there's probably a cheaper way to do that than a blockchain, but not one that guarantees the rules of the bounty(?).

Thinking along those lines, you'll definitely want to prevent submissions from declaring their own axioms (esp axiom unlimitedMoney := False -- I couldn't find your oracle code quickly, so I didn't see if you already covered that), and you'll probably want a system for the submitter to define their allowed axioms (is this a Euclidean- or Spherical- Geometry Proof?).

[Kim Morrison]

(You definitely don't want to allow any extra axioms in the Lean sense --- no one "adds axioms" to do euclidean or spherical geometry. :-)

[Kevin Buzzard]

(other than Euclid, Hilbert and Tarski)

[Johan Commelin]

Euclid, yes. But Hilbert and Tarski were both probably thinking of structure or class as opposed to axiom.

[Vadim Fomin]

The reason why I'm going for blockchain is to minimize trust issues. The submitters deserve to be sure that they will not be cheated out of their money, and it's in the bounty depositors' best interest, too, since otherwise there will be less submissions.
And it's cheap anyway. The gas fees are minimal. The costs of running the oracle and the virtual machine are all currently on my side, I doubt that it will change :sweat_smile:

[GasStationManager]

@John Wargo we do check the axioms used by the submission (see code). Only the three standard axioms are allowed: propext, Quot.sound, Classical.choice.

[Mario Carneiro]

The reason why I'm going for blockchain is to minimize trust issues

Going for blockchain is a good way to maximize trust issues

[Vadim Fomin]

Why?

[Mario Carneiro]

because the stakes couldn't be higher, you bring out the worst parts of people when every piece of code is its own bug bounty

[Mario Carneiro]

it's generally not a serious worry in the FLT project that someone will commit a axiom unlimitedMoney : False. Not so on blockchain

[Vadim Fomin]

I see what you mean. Yeah, when this thing takes off we really need a security audit for both the oracle and the smart contract. That's why I'm starting small with play money and inviting you all to participate. Right now you are extremely welcome to find any way at all to drain funds. Both the contract and the checker are open-sourced.

[Mario Carneiro]

and once you start looking at lean with an eye for making it an airtight sandbox, you will come out disappointed because that's not the model it was built on

[Vadim Fomin]

The submission is slightly inconvenient because you have to interact with blockchain, but I'm working on a web interface that will hopefully start bringing out the internal saboteurs in Lean enthusiasts :)

[Mario Carneiro]

you have to design for security and lean is not designed for security

[Vadim Fomin]

and once you start looking at lean with an eye for making it an airtight sandbox, you will come out disappointed because that's not the model it was built on

Yeah, I can already sense it, even though I'm a complete baby in Lean. But this has to be done anyway. No way Lean should have no way to safely check a proof's validity.

[Vadim Fomin]

Check out my contract here: https://github.com/wadimiusz/lean-contract-interact/blob/main/TheoremMarketplace.sol
And @GasStationManager 's checker here: https://github.com/GasStationManager/SafeVerify

[Mario Carneiro]

are you familiar with the story of the coq theorem bounty program that was taken down because people broke the system too often?

[Vadim Fomin]

I'm afraid not. I'd like to hear it :)

[Mario Carneiro]

previous discussion

[Vadim Fomin]

It seems silly to take down the program because of that, though. You just need to get the thing done. People offer bounties on Lean's zulip, the last time it happened was only a couple day's ago, if memory serves. It's within the mathemarical tradition. It's feels very natural to me to make it decentralized.

[Mario Carneiro]

I don't know what you are referring to, monetary bounties are not something we see on this zulip

[Vadim Fomin]

Here

[Vadim Fomin]

But I didn't express myself right, this was more of an isolated case that I saw, rather than a thing that happens frequently. Rather, I should have said that bounties on theorems have been a topic of discussion previously.

[Mario Carneiro]

it is amusing that one of the first exchanges there is about a kind of "cheating" which lean would have accepted

[Mario Carneiro]

so making the process fully automatic would have been a bad move

[Vadim Fomin]

Indeed. Your point about cheating is absolutely right; don't think I don't appreciate it.

[Mario Carneiro]

the thing is, this is the rule, not the exception. If you put money on a thing the first thing people are going to think about is how to cheat or otherwise circumvent the restrictions

[Vadim Fomin]

I agree.

[Mario Carneiro]

meaning that if you have a mathematical question and want a reasonable answer, money can actually hurt your chances of getting a satisfactory answer

[Vadim Fomin]

Unless I manage to set up a system in such a way as to align the incentives just right.

[Mario Carneiro]

The vast majority of questions asked on this zulip are answered by volunteers (like me!)

[Vadim Fomin]

I am not sure how successful the attempt will be, but I would like to try just to see what happens.

[Vadim Fomin]

I was actually thinking that a use case like "a frustrated Lean enthusiast doesn't know how to prove a basic lemma" may be a nice starting use case, and throw some meager money at starving grad students.

[Mario Carneiro]

there are incentive structures of course, I'm not doing this purely altruistically and my career would not be what it is without the support of the people who I have helped on this zulip

[Mario Carneiro]

Open source has its own way of supporting the people who get involved, it's just not as direct as a salary

[Mario Carneiro]

Anyway, what I'm saying is that if you make a bounty program you should not put much of value on it because it will be cleaned out several times

[Mario Carneiro]

especially if you build on a system that was not designed for security like lean

[Vadim Fomin]

I'm definitely planning for it. Like i said, that's why I'm starting with play money, and later I will use tiny funds.

[Vadim Fomin]

And I will invite people to seek vulnerabilities :)

[Vadim Fomin]

As a sort of red teaming.

[Vadim Fomin]

If this project ever becomes anything serious, it will need a security audit.

[Vadim Fomin]

I'm not sure anyone will ever care about this project, although I hope so very much.

[Vadim Fomin]

But if something becomes of it, a security audit will definitely be necessary...

[Niels Voss]

If the total amount of money remains small enough that getting it swept out by a proof of False every so often isn't a big deal, then regularly discovering exploits in Lean might not be the worst fate of a project, in that it's useful to know what kind of exploits Lean is susceptible to. If anything, I'm curious to see how this will go. I wouldn't however put too much faith in the idea that after an initial burst of flaws is discovered, Lean will be secure enough to not have proofs of False for years.

I would also think that using an external checker is probably necessary, because in the past there was a way to trick Lean's kernel with metaprogramming. Also keep in mind that Lean files can run arbitrary IO code when compiling, so be cautious about RCE exploits.

[Patrick Massot]

As Mario tried to explain, we are not discussing flaws in Lean here. We are talking about non-goals of Lean.

[Bolton Bailey]

Whether it's a goal "of Lean" or not, it certainly seems like it's a goal that some people in this thread have for Lean. I'd be interested to hear if there are other examples or formal languages that people think are more designed for security.

[Bolton Bailey]

As for why I personally am interested in Lean being used for this purpose, the answer is simply that Lean is the system I am most familiar with. Whatever people are saying in this thread about Lean not being designed for security, my feeling is that there is a level of effort that could be put in to make it sufficiently secure - it's just a question of what that level of effort is, and whether it will be attained, and whether (as is a legitimate worry) the bad situation will obtain where users think it has been attained and rely on it having been attained when it actually hasn't been.

Practically speaking, I imagine the SNARK links above are relevant to the question of how to make an adversarially robust formal system. This line of research already deals with an adversarial model. Moreover, putting a formal system inside a SNARK requires having a very simple environment for checking proofs, and I would think this process gets rid of many avenues for proving False. And clearly it has synergy with the "blockchain" aspect.

[Niels Voss]

I think the main concern is that with the amount of metaprogramming Lean supports, making it adversarilly robust will be fairly difficult, especially if it requires frequent PRs to core Lean, and it might just be low priority (or even a non-goal, as Patrick Massot said).

Maybe it will be more realistic to make one of the external proof checkers adversarilly secure?

[Vadim Fomin]

I want to have a theorem bounty system on blockchain, I'm flexible as to which checker to use. I just thought Lean was a good idea since it's all the rage and I hoped it would improve a mathematician's routine, but I can switch.

[Vadim Fomin]

No, that's not right. It doesn't make sense to just use any checker. I want to make something useful, something that can be integrated into a routine. Lean already has a routine, that's the nice thing, lean already has mathematics going on about it.

[Niels Voss]

By "external checker", I didn't mean another system that isn't Lean, I meant an external kernel for Lean

[Niels Voss]

Like https://github.com/digama0/lean4lean or https://github.com/ammkrn/nanoda_lib

[Vadim Fomin]

That would be neat - an external type checker should be good enough to verify bounties, right?

[Niels Voss]

I don't know about "good enough", but it's certainly better than not having one. You still might have to check for things like people adding extra axioms and making sure the theorem statement (and the terms that theorem statement depends on) have not been changed beyond what was requested

[Mario Carneiro]

Bolton Bailey said:

Whether it's a goal "of Lean" or not, it certainly seems like it's a goal that some people in this thread have for Lean. I'd be interested to hear if there are other examples or formal languages that people think are more designed for security.

Shameless plug, Metamath Zero is designed for security (or rather, provable correctness)

[Mario Carneiro]

I have used the theorem bounty situation as an example in my talks because I think it helps put people in the right mindset to understand what it means for a proof assistant to be provably correct

[Mario Carneiro]

If you are going to put a proof checker on the blockchain, use one like Metamath or HOL light or MM0, that is, one where "simplicity" is listed in the "pro" column. Don't use lean, it's just asking to get owned.

[Bolton Bailey]

Mario Carneiro said:

If you are going to put a proof checker on the blockchain, use one like Metamath or HOL light or MM0, that is, one where "simplicity" is listed in the "pro" column. Don't use lean, it's just asking to get owned.

Indeed, shameless counter plug for the work Pi squared (who I work for) is doing to but proofs in metamath on the blockchain.

[Kim Morrison]

There's also the annoying problem, already well in evidence above, that people will (ignorantly or wilfully!) mistake "this blockchain proof checker based on Lean accepted a proof of False" for "Lean/lean4checker accepted a proof of False".

Please don't exacerbate it?

[Vadim Fomin]

I'll try my best not to frame anything like that. Anything like bounties for False will be bug hunt on our side. Of course, it's technically possible that a bug in Lean could be found, but a bug in the checker implementation is overwhelmingly more likely, especially in an adversarial setting. I won't make it Lean's problem, don't worry.

[Kevin Buzzard]

You won't, but the media might

[Vadim Fomin]

Is that a thing that's happened to the Lean community, ever?

[Adam Kurkiewicz]

A friend participated today in a hackathon in Berlin organised by people behind this:

https://www.cairo-lang.org/
https://github.com/zksecurity/stone-cli

It seems on-topic @Vadim Fomin , but I don't know much about it, and I didn't attend the hackathon.

From a cursory look, it seems like the purported innovation is running long programs off-chain for efficiency, but with semantics of on-chain execution (and with some level of formal guarantees).

[Vadim Fomin]

That seems very relevant indeed, thank you!

[Adam Kurkiewicz]

@Vadim Fomin how would you prevent the front-running that @Bolton Bailey mentioned earlier in the thread?

I think the solution would have to involve committing a hash of the proof (or some other evidence of priority) on-chain, and then a settlement period when anybody can claim priority by referencing the hash, and the proof with the earliest hash wins. Although maybe a smarter scheme can be invented.

[Bolton Bailey]

I mean if you are going to involve zk-SNARKs you can do things in one round by signing the proof and then making a zk-SNARK proof you signed it (but people will probably then complain that not revealing the proof is something you want to prevent)

[Vadim Fomin]

I'm not sure yet. I'm really trying to do baby steps here, doing some minimal thing that works and then iterating it. I haven't even published a website interface of the smart contract yet (sorry folks, I was sick; but i'm getting there). Can't we just, like, encrypt submissions so that someone seing your submitted transaction can't ape it in their own name, and indeed see what you submitted, and then we just trust the ordering of blocks?

[Adam Kurkiewicz]

@Bolton Bailey could you elaborate? I don't understand those ZK-SNARKs. I tried to read a bit, but I still don't really get it. Who verifies that the proof exists and is correct? There is a computation to run to verify the formal proof, so that needs to run somewhere somehow. If the computation runs without the program getting revealed then that's homomorphic encryption? And then there is a question of authorship. Why wouldn't somebody just take the proof and front-run it with their own signature? I don't really understand how this all fits together.

[Adam Kurkiewicz]

@Vadim Fomin committing one hash to a blockchain is cheaper than committing the entire (encrypted) proof, and it's just as good a proof of authorship as an encrypted proof. So I think using a hash is a better idea than using encryption. Bolton's idea is probably better yet, I just don't understand it.

[Vadim Fomin]

That makes sense. Probably the thing that actually matters is not the purity of the concept but the convenience to the users, so, in practice, how cheap it will be to submit, how reliable the web interface will be, and how secure against attacks. That is, if I want it to actually help anyone with their Lean lives.

[Bolton Bailey]

Adam Kurkiewicz said:

Who verifies that the proof exists and is correct? There is a computation to run to verify the formal proof, so that needs to run somewhere somehow.

The verification procedure is run by the person who creates the Lean proof. To vastly oversimplify, they run the Lean verification procedure on a virtual machine and write out the entire trace of the state of that virtual machine and then apply fancy error-correcting codes to that data, and then create a cryptographic summary of all of that that guarantees that the final state of the virtual machine was e.g. "x^n + y^n + z^n /= 0 was successfully proved in Lean". The cryptographic summary then guarantees that this was the final state without anyone having to re-run the computation.
Adam Kurkiewicz said:

If the computation runs without the program getting revealed then that's homomorphic encryption?

FHE is related but not the same. EDIT Perhaps a good explanation would be that in FHE, the details of the proof are kept secret from even the computer running the verification procedure, which doesn't have to happen here, since we assume the cryptographically protected verification procedure is being run by the one who made the Lean proof.
Adam Kurkiewicz said:

And then there is a question of authorship. Why wouldn't somebody just take the proof and front-run it with their own signature?

What I am suggesting is that instead of running just a program that checks the Lean proof, we run a program which checks the Lean proof, and then also receives as input a public key and directly outputs that same public key. The "ARK" stands for "argument of knowledge", it basically means that whoever created the SNARK had to know a set of inputs that made the program output the way it did. Someone wanting to substitute their public key with the prover's will not know the proof and will not be able to construct a new SNARK that corresponds to the output simultaneously containing their public key and outputting "x^n + y^n + z^n /= 0 was successfully proved". (as long as the SNARK is not malleable, yada yada ...)

But I agree that all of this is much more advanced than a minimal prototype would look like.

[Adam Kurkiewicz]

Oh wow, I didn't realise that this was already technologically possible?

The "ARK" stands for "argument of knowledge", it basically means that whoever created the SNARK had to know a set of inputs that made the program output the way it did.

And those inputs can, in principle, be virtual machine opcodes? So that the smart contract contains (publicly visible), statement of the theorem and the public key claiming "ownership" of the formalisation, and the "inputs" is the actual formalisation of the proof of the theorem, which are then cryptographically proven to lead to a (non-malleable) virtual machine state that certifies the existence of the proof.

Am I understanding this right?

[Bolton Bailey]

Yes, that is all correct

[Adam Kurkiewicz]

I think we would like to know the theorem though (in the traditional sense of e.g. Erdos bounties), so that's still a two-phase protocol

[Adam Kurkiewicz]

Unless you've got more cryptographic cleverness I didn't know existed :)

[Bolton Bailey]

Time delay encryption would be the obvious candidate

[Adam Kurkiewicz]

OK, but from an engineering point of view probably having 2 or even 3 phase protocol is probably fine. It will work. If I were to build something like this for real, I would probably like to keep it as simple as possible

[Bolton Bailey]

At the risk of hijacking discussion even further (sorry @Vadim Fomin ) there is a continuation to the arms race where the prover can avoid revealing the proof by obfuscating it (i.e. making the proof convoluted in a cryptographically undecipherable way). I think there is an interesting mechanism design question on how to incentivize prosocial theorem proving. For example, if someone creates de novo an interesting lemma, that no one anticipates, but goes on to be critical in the proof of several bountied theorems, how can we ensure that the creator gets a share of the reward.

[Bolton Bailey]

As a further thought about practical failsafes: If we are worried about it being possible to prove False with whatever checker we have, one possibility is to delay all payouts on all bounties for a week or so and have smart contract return control of funds to a multisig if a proof of False is ever discovered. The idea being that if someone does prove False and uses that proof to prove other falsehoods, white hats can potentially protect the account from being drained by understanding the faulty proof and triggering the failsafe.

[Vadim Fomin]

For example, if someone creates de novo an interesting lemma, that no one anticipates, but goes on to be critical in the proof of several bountied theorems, how can we ensure that the creator gets a share of the reward.

I've been thinking about this a lot. I don't have great solutions here. This feels like it should be a feature of the market eventually. Maybe this will at least partially be solved with market dynamics, not technology. For example, imagine that there is a huge bounty placed on proving A -> B, and C -> B is trivially shown, so an almost equal bounty is placed on A -> C; and when A -> C is submitted, the requester of the proof A -> C submits proof for A -> B. But this doesn't work for the lemmas that no one anticipated, like you said.

[Adam Kurkiewicz]

Oh these are interesting considerations, you clearly thought about this quite deeply! A quick question about ZK-SNARKs, how scalable is on-chain verification of those? Is there some log(n) penalty that the chain has to pay, where n is the number of steps in the formal proof, or is 100% of the computational cost on the off-chain verifier who produces the ZK proof of running the SNARK?

[Bolton Bailey]

Adam Kurkiewicz said:

Oh these are interesting considerations, you clearly thought about this quite deeply! A quick question about ZK-SNARKs, how scalable is on-chain verification of those? Is there some log(n) penalty that the chain has to pay, where n is the number of steps in the formal proof, or is 100% of the computational cost on the off-chain verifier who produces the ZK proof of running the SNARK?

I'm glad you asked! The answer is that some zk-SNARKs have cryptographic-proof-verification-procedures with O(log(n)) cost with a large constant, but efficient cryptographic-proof-generators, and some SNARKs have inefficient cryptographic-proof-generators but very fast cryptographic-proof-verification-procedures . In practical terms, if you have a zkSNARK that is expensive to verify you just ... Make a latter ZK-SNARK of the former ZK-SNARK's cryptographic-proof-verification-procedures. This is not a joke, it's literally what the state-of the art systems all do.

[Bolton Bailey]

Unfortunately I am not an academic anymore, otherwise I would give a rump session talk about the infinite binary tree in which the left-child of any node is "apply a SNARK to it" and the right child is "formally verify it". Every node in the first two levels of this tree has a realization in code.

[Adam Kurkiewicz]

Just to make sure I'm following: verifier is the on-chain program that checks the ZK-proof, and the "prover" is what happens locally e.g. how the formalisation gets checked on the VM.

[Bolton Bailey]

Yes, sorry, obviously terminology here is confusing, will edit

[Bolton Bailey]

As for practicality, google tells me 200,000 to 500,000 gas to verify a SNARK on ethereum. At current prices, seems like thats about $18. Of course there are proposals and debates to make it cheaper :shrug:

[Adam Kurkiewicz]

Nah, all good, it's just not my field at all, so I'm learning the terminology.

[Adam Kurkiewicz]

I'm still struggling to understand this:

Make a latter ZK-SNARK of the former ZK-SNARK's verification procedure

Can you elaborate?

[Bolton Bailey]

Well, it's specifically confusing because there are two notions of "proof" - formal proof, and cryptographic proof.

Adam Kurkiewicz said:

Can you elaborate?

Just as we can make a zk-SNARK that runs the program which is lean's kernel and outputs "someone knows of the existence of a proof of this mathematical statement which was valid according to lean's kernel", we can make a zk-SNARK that runs the program which is "another SNARKS cryptographic-verification-procedure" and outputs "someone knows of the existence of string of data which is a valid cryptographic certificate of as checked by this SNARKs cryptographic-verification-procedure, and which, according to that procedure, says "someone knows of the existence of a proof of this mathematical statement which was valid according to lean's kernel"".

[Bolton Bailey]

We are now at the third level of the tree I was describing above.

[Adam Kurkiewicz]

Ah I see, so the idea is that basically at this stage with the nested ZK-proofs, you are paying O(log(log(n) + C) + C), where C is the large constant. The inner large constant would need to to be paid by whoever wants to verify the inner ZK-proof, but nobody really needs to verify it as verifying the outer ZK-proof is sufficient, so effectively the chain will pay only approximately log(log(n)) + C of the outer proof

[Bolton Bailey]

Adam Kurkiewicz said:

Ah I see, so the idea is that basically at this stage with the nested ZK-proofs, you are paying O(log(log(n) + C) + C), where C is the large constant. The inner large constant would need to to be paid by whoever wants to verify the inner ZK-proof, but nobody really needs to verify it as verifying the outer ZK-proof is sufficient, so effectively the chain will pay only approximately log(log(n)) + C of the outer proof

This explanation makes it sound like the inner C and the outer C are the same. It's not quite true that no one needs to verify the inner snark, the prover has to verify it in the process of constructing it. Here is a numerical explanation (All of these numbers are too small, but this gives the idea)

There is one SNARK "CAIRO" which takes

• 1024 t log t time to prove the result of a program that took t time to run on its own,
• and the proof verification procedure takes 4096 log t time to run.

There is another SNARK "GROTH16" which takes

• 65536 t log t time to prove the result of a program that took t time to run on its own,
• and the proof verification procedure takes a constant 128 time to run, no matter the program execution length.

What we do is run the CAIRO SNARK, and then run the GROTH16 SNARK on the proof verification procedure of CAIRO. We get a new SNARK, which we might call GROTH16(CAIRO):

• Proof time = Time to prove initial program using CAIRO + Time to prove resulting proof verification in Groth16 = 1024 t log t + 65536 (4096 log t ) log (4096 log t ) (note that the first term dominates for large enough t).
• Verification time = 128, since, as you say, verifying the outer SNARK is sufficient.

[Adam Kurkiewicz]

And t is the number of opcodes for the virtual machine?

[Bolton Bailey]

t is the number of times it executes an opcode, in other words the number of "cycles", yes.

[Adam Kurkiewicz]

I see, very interesting technology. Thanks for explaining Bolton! It's a neat trick with nesting the SNARKs

[Adam Kurkiewicz]

And the soundness/correctness of these systems is generally quite high I assume? Something similar to Bitcoin/Ethereum? Or are they way more experimental than that?

[Bolton Bailey]

That is itself an interesting question. While in principle you can scale up the security parameter, the security parameters in practice are not always chosen well, though I haven't heard of anything being broken because of this. There are a variety of cryptographic assumptions at play. In some cases the security relies on conjectures in coding theory.

[Adam Kurkiewicz]

One idea to promote a system capable of providing these kind of bounties would be to offer "Erdos bounties" on all the unsolved Erdos problems . This seems timely given that the informal custodian of Erdos bounties passed away a few years ago (I don't know any more details of this than what's on the internet, but there are many mathematicians in this forum, so they might know more):

https://en.wikipedia.org/wiki/Paul_Erd%C5%91s

There are thought to be at least a thousand remaining unsolved problems, though there is no official or comprehensive list. The offers remained active despite Erdős's death; Ronald Graham was the (informal) administrator of solutions, and a solver could receive either an original check signed by Erdős before his death (for memento only, cannot be cashed) or a cashable check from Graham.[49][needs update] British mathematician Thomas Bloom started a website dedicated to Erdős's problems in 2024.[50]

Details of a recently paid out bounty:

https://nautil.us/cash-for-math-the-erdos-prizes-live-on-236641/

The list of problems Erdos offered cash for appears to be here (and the curator of the list @Thomas Bloom is on this Zulip chat) :

https://www.erdosproblems.com/prizes

This would apparently require 33,817 USD worth of funds (in 2024 dollars). If we were to adjust for inflation from 1985 dollars, we would be talking about ~3x that money so about ~$100k USD.

I can imagine that a crypto company or a crypto philanthropist might be willing to provide this level of funds if you could get the underlying technology working properly, even if just for publicity/marketing reasons (One of them recently bought a banana for $6.2m USD...). From the conversations so far it seems like using ZK-SNARKs and using Metamath Zero or similar (as opposed to lean) are all good ideas.

[Vadim Fomin]

Erdos was specifically one of the sources of my inspiration :)

[Vadim Fomin]

Is there a linter for Lean that works online, so that I could reject theorem requests and submissions in bad Lean? natural numbers game had something like this, right?

[Vadim Fomin]

I mean, I can just reject them on the server side, but maybe it can be done in the browser already?

[Kevin Buzzard]

Stick #lint at the bottom of your file. And no, I don't think NNG had anything to do with linters (indeed the author of NNG had no clue about what a linter was when that game was first written)

[Vadim Fomin]

I meant more like, do I have to send the file to the backend to check if it compiles or can I do something right in the webpage?

[Kevin Buzzard]

Oh I see, you just want to know if the file compiles without errors?

[Vadim Fomin]

Yeah.

[Vadim Fomin]

Alright, so I made a website for playing around with that smart contract: https://theorem-marketplace.com

You just need to install MetaMask (here, or click the button on the site), and some play money ("Sepolia Ether"; I can wire you some, that's the easiest way, or you can get it from online faucets)
Feel free to play around with it and break it in any way you can think of :)

It supports Mathlib - just write "import Mathlib".