Lean and blockchain

Stream: new members

[Huỳnh Trần Khanh]

What does Lean have to do with blockchains? It seems that quite a few blockchain people are interested in Lean and theorem proving in general.

[Lars Brünjes]

Blockchains are high-assurance systems whose correctness is absolutely crucial - billions of dollars can be lost if there is a bug. This makes blockchain technology an ideal domain for formal methods, formal verification and thus machine-checked theorem proving.

Apart from that, it would be cool to have something like "mathlib on the blockchain", where theorems would be persisted on a blockchain and nodes would validate the proofs. Over time this could grow into a universal, formally verified global decentralized library of all of mathematics.

[Eric Wieser]

Decentralizing things feels like an anti-feature - a decentralized library feels indistinguishable from a collection of incompatible libraries to me. Encoding 50 different definitions of a group in a blockchain doesn't help anyone!

[Kevin Buzzard]

For my sins I am now on the International Mathematical Union's committee on Electronic Information and Communication, which is supposed to be leading on some kind of Global Digital Mathematics Library. We just had a meeting about it. Eric will be pleased to hear that blockchains weren't mentioned once :-)

[Huỳnh Trần Khanh]

I also detest blockchains, count me in! I don't really understand what threat model it's trying to mitigate.

[Julian Berman]

https://eprint.iacr.org/2017/375.pdf

[Julian Berman]

(or the shorter version, http://doyouneedablockchain.com/ )

[Lars Brünjes]

Decentralization does not mean chaos - the whole point of blockchain is to have a decentralized system (hence a system that is not controlled by a single entity) which has consensus, i.e. agrees on what content is valid and what is not.
The "threat model" is special interests, dictatorial governments, censorship and any other entity that wants to control access and information.
Decentralized just means that blockchains are highly resilient - both against technical problems (earthquakes, floods, fires) and against deliberate attacks. Such a library of mathematics on the blockchain would be under nobody's control and would belong to the whole world, not a single country or university or company. I think that is definitely a desirable state of affairs.

[Mario Carneiro]

I'm curious how you envision refactoring happening in such a model

[Lars Brünjes]

Good question - blockchains are "write only", that's sort of the point...
That being said, such a system would of course need some kind of incentives model. One idea I had a while ago was that you have to pay transaction fees for uploading content, but if you reference existing results, part of your transaction fees go to the creator of those results. That would incentivize people to prove "useful" things - like the fundamental theorem of calculus or Zorn's lemma or the Yoneda lemma. The hope would be that by carefully calibrating such incentives, people would be guided into the "right" direction.
With such a model, I would imagine that "refactoring" would be realized by somebody coming up with a better formulation or more general version of a previous result, and others would then rather cite this improved version instead of the old one.
Old content would always be there, but references would start pointing to the new, improved version.

[Johan Commelin]

@Lars Brünjes Currently we have completely different problems than what a blockchain would solve, I think. Currently we have roughly 30 ~ 40 people that care about moving this library forward. The rest of the world barely knows it exists.
If 2 or 3 people work hard on redesigning a part of the library that caused friction, there is a cooperative discussion here on Zulip on how to best solve the issue. We try to reach a consensus, merge the PR, and move forward.

These 30 ~ 40 people are scattered across the globe, and all have a complete git history of the project on several devices. I think this protects us well enough against natural disasters as well as against any nation state trying to corrupt or censor whatever we do.

If github decides to ban mathlib, we have a slight problem. But githubs features aren't can't be replaced by a blockchain, I think. They need to be replaced by a good online git forge. Something like gitlab or sourcehut, probably.

[Lars Brünjes]

@Johan Commelin I certainly admire the effort you guys put into this project, and even though I work for a blockchain company, I am the last one to claim that blockchain is the answer to all problems. I only tried to answer @Huỳnh Trần Khanh 's question about why so many blockchain people are interested in automatic theorem proving.

That being said, I do believe that by moving a system like Lean onto a blockchain, you would potentially attract orders of magnitudes more people to it than the 30-40 you have now. I would imagine that part of the problem with systems like Lean - cool as they are - is their ephemeral nature. If I put all this time into proving a theorem in Lean, how long will that proof last until Lean is replaced by a new, not downwards-compatible version? I do not think that this is the only problem, but I do think it's part of the problem. It's great fun to play with Lean, but is it a "future-proof" investment? I think it is fair to at least be somewhat sceptical.

Again, I don't want to criticize the great work you guys are doing here. Lean is awesome and great fun!

[Mario Carneiro]

That would incentivize people to prove "useful" things - like the fundamental theorem of calculus or Zorn's lemma or the Yoneda lemma.

Actually I think with this cost model you would be much better served to prove add_assoc

[Mario Carneiro]

"big" theorems are referenced way less than the piddly stuff in algebra

[Lars Brünjes]

Sure - agreed. But that's good - get all the boring, but extremely useful results out there as fast as possible, so we can concentrate on proving fun results.

[Mario Carneiro]

Mathlib is not an archive, it is a curated mathematical library. I think this model is more appropriate for a journal-style system like AFP (archive of formal proofs, in isabelle) or JFM (journal of formalized mathematics, in mizar)

[Mario Carneiro]

but here the point is that you don't "own" your theorems, you are contributing to an evolving project. Ownership would get in the way

[Mario Carneiro]

in particular old projects by people that have moved on is a big drag on forward progress in journal style projects

[Mario Carneiro]

If I put all this time into proving a theorem in Lean, how long will that proof last until Lean is replaced by a new, not downwards-compatible version?

With any luck, not long (lean 4 is on the horizon). But the point of continuous evolution is that even if your result has to be updated it will still exist in future versions of the library. With an archive style it is really easy to just leave this old stuff behind, and I think that's bad because then you have to go find an outdated version of the tool and/or supporting library to get this result compiling

[Eric Wieser]

Note that we already have a partial tool for deciding "which content is valid and which content is not" - it's the lean compiler, which rejects invalid proofs. Of course, mathlib can still become contaminated with an "incorrect" definition, but that can happen even if contributors have good intentions

[Kevin Buzzard]

A blog post I wrote recently went to the top of Hacker News yesterday and this usually has the consequence that people send me a bunch of stuff. Here's something on ArXiv sent to me by Clément Hongler that mentions both Lean and blockchain and which seems to be a sensible contribution rather than the hype-fests we sometimes see.

[Meve Rai]

I also work in the blockchain space and have also played with theorem provers in the past, although I am very uninformed when it comes to this area...
However I would like to add a few things to this discussion:
What can blockchains do for systems like Lean?
One use case I have been thinking about, and I think is doable today with some effort, goes something like this:
You could use blockchains to steer research, by directly providing incentives for certain theorems. How this process works at the moment: tax money goes to senior people in Maths departments, they decide what is interesting, and then use this money to incentivise themselves/their department/their students to work on this interesting stuff. Weather they were successful in their efforts, i.e. did they get a proof for their theorem, is decided by peer review.
You could replicate this process on the blockchain: funding is directly attached to some type T. First person to show a term of type T collects the funding. In this model anyone can fund the theorems they wanna see proven, and peer review is replaced by the Lean type checker.
I can imagine in this model, with some editor integration, you are working on some proof, but there is this one lemma you can't prove. Then in your editor you issue some command and a bounty on this lemma is sent to a blockchain (you have to fund it of course). If someone proves it, your editor notifies you and you can import this term.
A side effect of this a collection of theorems stored on the blockchain.
Now implementing this is quite a technical challenge. You can't actually type check term on chain, that would be too expensive. But there are tricks you can use to essentially verify a typecheck, by only running one step of the Type-checker machine. But this again requires you to come up with a cryptographic commitment scheme for your Lean terms.
I was thinking of starting this project, but my knowledge about Lean and similar languages is quite limited, so I kind of put it on hold. If anyone here is interested in working on this, let me know...

[Mario Carneiro]

What if half of the work is coming up with the theorem statement? In most industrial scale verification efforts it's not like someone hands you a fully elaborated and correct theorem statement and asks you to prove it, rather while you are working on the proof you are also refining the statement, and 99% of the time the first draft theorem statement was wrong for trivial reasons

[Mario Carneiro]

If you stake money on a theorem and it turns out to be true for the wrong reasons, you will feel swindled

[Meve Rai]

I see. As I said I am not well informed in the area, the idea above sounds good from what little I understand about these systems. Is the problem you describe unique to industrial verification, or does it also appear when trying to do pure maths? I would think there is less room for variety in stating theorems when it comes to pure maths vs. when trying to argue for correctness of some software system. Or is that not the case?

[Huỳnh Trần Khanh]

what if there are a lot of types that are incompatible but still state basically the same thing? i guess this will happen: first person to show a term of type T0 collects the funding, then a bunch of people see the original T0 proof and then try to transform the T0 proof into T1 proof, T2 proof and so on and so forth and collect the funding for other equivalent types? so this is basically the same as a typeracer race and i don't think this is really fair to the T0 person

[Huỳnh Trần Khanh]

my personal conviction is that relying on a mindless autonomous system such as a blockchain to replace a well-established social process is fundamentally a bad idea

[Mario Carneiro]

Is the problem you describe unique to industrial verification, or does it also appear when trying to do pure maths?

It happens in pure maths too but people are less willing to stake a considerable amount of money on pure maths theorems

[Mario Carneiro]

If it's just a small issue that comes up in a proof you are better off coming to a support forum or chat platform like this one

[Mario Carneiro]

I don't see the motivation to do microtransactions for this sort of thing

[Meve Rai]

Huỳnh Trần Khanh said:

what if there are a lot of types that are incompatible but still state basically the same thing? i guess this will happen: first person to show a term of type T0 collects the funding, then a bunch of people see the original T0 proof and then try to transform the T0 proof into T1 proof, T2 proof and so on and so forth and collect the funding for other equivalent types? so this is basically the same as a typeracer race and i don't think this is really fair to the T0 person

Well if there is funding on T1, I don't see why that would be a problem. If T1 is a simple transformation of T0, and someone put a lot of funding on T1, they are just lazy. However I do think it would be interesting to pay fees on assumptions. If T1 uses T0 as an assumption, whoever solved T0 could collect a % fee on the bounty of T1.

[Meve Rai]

Mario Carneiro said:

I don't see the motivation to do microtransactions for this sort of thing

Could be a fun game though. If you are good at Lean you sit in front of your computer all day and prove random theorems for money :)

[Meve Rai]

Huỳnh Trần Khanh said:

my personal conviction is that relying on a mindless autonomous system such as a blockchain to replace a well-established social process is fundamentally a bad idea

I am under no illusion that this sort of system can replicate all that the current system provides. It would be an interesting experiment though. It becomes even more interesting if you imagine a world where the players playing these games aren't human, but machine...

[Kevin Buzzard]

With mathematics I would say that we are far more likely to be able to construct a fully elaborated and correct theorem statement first time round and it's 99% likely to be correct rather than incorrect, eg Fermat's Last Theorem, however there is no "pay per theorem" model in pure mathematics because typical interesting conjectures are so hard that you ask for funding to make vaguely specified partial progress on big problems and often your main results are "we proved X subject to the following technical constraints which we couldn't have guessed would show up five years ago". It's then up to the community to judge the value of this progress. The goals of blue sky research are often vague, you don't put in a grant proposal saying "I will prove the Riemann Hypothesis", you propose developing strategies that might help. I would say more generally it's very rare that someone comes along with a grant proposal saying "I will prove precisely X" and then goes away and proves precisely X.

[Meve Rai]

Kevin Buzzard said:

With mathematics I would say that we are far more likely to be able to construct a fully elaborated and correct theorem statement first time round and it's 99% likely to be correct rather than incorrect, eg Fermat's Last Theorem, however there is no "pay per theorem" model in pure mathematics because typical interesting conjectures are so hard that you ask for funding to make vaguely specified partial progress on big problems and often your main results are "we proved X subject to the following technical constraints which we couldn't have guessed would show up five years ago". It's then up to the community to judge the value of this progress. The goals of blue sky research are often vague, you don't put in a grant proposal saying "I will prove the Riemann Hypothesis", you propose developing strategies that might help. I would say more generally it's very rare that someone comes along with a grant proposal saying "I will prove precisely X" and then goes away and proves precisely X.

Do I understand correctly though, that these elaborations/strategies you develop often inform about what is needed to prove precisely X? What I mean is, say people agree that a proof of Riemann hypothesis is valuable, and there is large bounty on it. You then realise that knowing X,Y and Z could lead to a proof the Riemann hypothesis. This in turns means that now X, Y and Z should obtain some value. But I do imagine these elaborations are often difficult to state formally.

In any case I think this opens up an interesting debate about wherein precisely lies the value of pure maths research. Is it in possible applications years/decades/centuries down the line? Is it more like art, some transcendental sort of thing? I think this question is actually important, since pure maths research is in part being funded by tax-payer money. And if one believes in the "will of the people", I think mathematicians have some accountability to "the people" to produce such results that maximise some common utility.

The idea behind systems like this is to create mechanisms to steer the massive brain power that mathematicians posses towards some goal that is determined partly outside their control...

[Kevin Buzzard]

Nobody has a clue where the next big breakthrough is coming from. There were plenty of people interested in Fermat's Last Theorem in the 80s and early 90s and even after Ribet's work showing that it followed from a hard conjecture in arithmetic geometry (Taniyama-Shimura) it still wasn't clear to the community that this was the way it was going to be solved, there were people trying to crack it via ABC and transcendence methods for example, and Taniyama-Shimura seemed out of reach anyway. If you had asked mathematicians the week before Wiles' announcement which would be proved first out of Taniyama-Shimura and Birch--Swinnerton-Dyer you would have got random answers, but TS is now ancient history and BSD remains unproved. Similarly nobody seemed to know that Poincaré world succumb to a Ricci flow approach. People just chisel away and occasionally something big randomly breaks off, but 99.9% of research is more chiseling and proposals indicate targets but often don't claim they'll completely resolve a big theorem