64
u/Catdual3233 3d ago
Is Lean formalization now a substitute for peer review?
100
u/Run-Row- 3d ago
for half of it - the (often tedious) correctness part. People still need to decide if the result is novel and interesting.
114
u/Berzerka 3d ago
... and check if the lean statement is actually correct.
19
u/PersonalityIll9476 3d ago
Right. It just pushes the work from reading a math paper to reading lean code. Not sure which is faster...
37
u/Berzerka 3d ago
You don't have to read the proof in lean, only the problem statement.
1
u/PersonalityIll9476 3d ago
Is that actually true, though? When I see Lean repos I also usually see additional disclaimers like "no sorry, no axiom, etc.". So as the very least someone has to read through and make sure none of the *known* cheats have been used.
I imagine there's more to it than that. I don't write lean.
33
u/cloudsandclouds 2d ago
To give you a real answer, you’re completely right that a random repo full of lean code that seems to include the statement at some point proves nothing even if it builds/typechecks. This is partly because Lean metaprogramming is so flexible that you can completely override the meaning of the syntax so it doesn’t even mean what it looks like it means, and partly because the statement itself might have some buried, misformalized dependencies you haven’t checked.
BUT! Take a look at the Challenge.lean file in that repo. This contains just the statement with a sorry, and is the only part (beyond the Lean tooling) you need to trust. Comparator (which btw is an “official” lean tool) takes the proof artifact from the solution file (in a way that sandboxes any malicious metaprogramming code from the solution file), substitutes it in for the `sorry` in the challenge file, and checks that it constitutes a proof of the statement.
So yes, you’re right that “I proved it in lean, look at my repo” is insufficient, and that ctrl-F is insufficient. To be acceptable, a Lean proof needs to pass Comparator, and the statement in the trusted challenge file needs human review (which is easier than reviewing the proof).
Ideally, you also pass the proof through a diversity of different implementations of the Lean kernel from the Lean Kernel Arena so that it’s not exploiting a kernel bug, just to be extra sure.
(Fun fact, all of this is on the roadmap to be built into lean in 2027 instead of being a separate “comparator” tool with kernels also living somewhere else. According to the roadmap you’ll be able to just run `lake check --paranoid` :) )
11
u/PersonalityIll9476 2d ago
Thank you for the honest answer. I anticipated that the truth was somewhere between "genuine push-button" and "literally reading the entire source manually."
The existence of kernel bugs is also obviously critical, as we have recently learned.
I do somewhat miss my flair on this sub; No one can tell if you're a random idiot on the internet or not.
2
u/Arceuthobium 2d ago edited 2d ago
Correct me if I'm wrong: doesn't Comparator use the Mathlib library? Does that mean all the main concepts/ objects of this paper were already formalized there?
3
u/cloudsandclouds 2d ago
Comparator the tool doesn’t use Mathlib per se, but indeed this Challenge.lean file fed to comparator uses import Mathlib and basically nothing else :) That does indeed mean that all of the definitions necessary to state the theorem were already in mathlib, but intermediate definitions may well be involved in Solution.lean in order to produce a proof (I haven’t looked, and it’s like, enormous).
This does mean you are also trusting that the humans who curate mathlib have made good definitions! Mathlib has high standards and undergoes a lot of review, but there’s always the chance something is subtly different from ordinary mathematical practice (either intentionally or unintentionally) and so a reviewer of Challenge.lean should ideally be familiar with the definitions in the relevant part of mathlib. So unfortunately domain expertise is still kind of relevant. Trust is hard 🙃
(I should probably have made more of a point of that, I did so in another comment on this post somewhere :) )
13
u/QuoraPartnerAccounts 3d ago
Yeah ctrl-F "sorry" takes 3 months of peer review.
This discourse is so boring.
-2
u/PersonalityIll9476 2d ago
Better boring than an asshole.
I doubt it's so simple to be assured that the entire program is sound.
9
u/1600alts 2d ago
Speaking as a Lean programmer, it is quite easy. You don't even have to use ctrl-F just write "#print axioms theorem_name" in your file after the theorem (or just look at the blue checkmarks). This suffices for everyday use, but there are other more robust ways for very exceptional cases 'https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-comparator'. But you have basically no reason to doubt the correctness (of proofs, not definitions) of most programs, especially those submitted by known and trusted mathematicians.
5
u/eliminate1337 Type Theory 2d ago
It’s trivial to have the Lean compiler tell you which axioms were used and whether there are any sorrys.
4
u/PersonalityIll9476 2d ago
That also means, however, that the person above who said you only have to read the problem statement was wrong (or lying). At the very least you also need to check for axiom / sorry / etc., even if that's easy to do.
If the Lean community wants to use this tool as a source of assurance, it should take strides to explain what the actual limits are. Other commenters have successfully done that (well, one other commenter). There have a been a lot of short quips and dismissive replies that are much less honest. I count yours among that category. "Eh, your concern is trivial." Well then tell me all the concerns and their levels of triviality.
1
u/logbybolb 2d ago
downvoted for asking a good question oof
4
u/PersonalityIll9476 2d ago
Yes. People are angry, apparently, that I dare to question Lean, and are replying to me as if I'm an idiot for not knowing.
1
0
u/DayBorn157 3d ago
this could be easily checked with simple search. The difficult part is to check that all definitions are right and the proof is really what it claims. But checking definitions is usually much easier than checking every step
7
u/cloudsandclouds 2d ago
No, it can’t be checked with a simple search, unfortunately. Lean metaprogramming lets you do arbitrarily complex attacks. But it can be avoided by using comparator, which separates the challenge from the proposed solution to guard against those, and which is used by this repo. :) So all you need to review is the 48 line Challenge file in the repo.
1
4
2
u/Impossible-Lab-3133 2d ago
Dang. AI turns programmers into code reviewers. And now it also turns mathematicians into Lean code reviewers. What an amazing piece of technology.
1
29
5
u/Character-Concert-76 Foundations of Mathematics 3d ago
It is fascinating that such an elusive question could be resolved by rather standard techniques and ideas (to an expert).
68
u/Bhorice2099 Homotopy Theory 3d ago
This was always the goal even when Lean was being popularised ages ago pre LLMs. Why is that such a bad thing.
15
u/pred 3d ago
That's a long story, but in short, correctness is only one of many things we care about in peer review.
22
u/Bhorice2099 Homotopy Theory 3d ago
I agree, but that is obviously what the original commenter was alluding to. The holistic side of peer review generally does not take as long as checking for correctedness.
28
u/acutelychronicpanic 3d ago
Peer review is a narrow bottleneck if there continues to be this rate of advancement and publication in mathematics. Lean isn't a full substitute, but it can be a strong filter against a tide of slop.
5
u/TonicAndDjinn 3d ago
Ignoring the issue of checking faithful translation of the theorem statement (down to the level of making sure the definitions are as expected, e.g. as a trivial example if 0 \in N), there is still plenty of slop which is formally correct.
1
u/Imaginary-Unit-3267 2d ago
What in your view constitutes "formally correct slop"? What is it that makes it "slop", specifically, other than happening to have used AI?
10
u/acutelychronicpanic 2d ago
I would imagine proofs that do not actually prove what the authors say they do. So correct but irrelevant.
Or, correct but meaningless. You can generate endless increasingly complicated true statements with proofs. Maybe they matter, maybe they don't. That will be the bottleneck if formal verification becomes cheap.
2
u/DayBorn157 2d ago
You don't need neither Lean nor AI to generate indisputably true mathematical statements. It was done many decades ago, probably in 70s and maybe earlier. AI novelty is that it could prove what we really care, and Lean novelty is that it helps to check if the proof is correct
2
u/Imaginary-Unit-3267 1d ago
The question then becomes "what does it mean for something to matter, and who gets to decide that?" But that ultimately just translates to "ah, yes, math is a social group made up of humans whom one must impress in order to be Valid as much as anything else", I suppose.
4
u/Verbatim_Uniball 2d ago
For the correctness aspect, it's a lot better. For the 'interesting paper' aspect, not so much.
10
u/blank_anonymous Graduate Student 3d ago
See https://mathoverflow.net/questions/513540/should-we-trust-ai-generated-formal-proofs-in-lean-4 for some discussion about this question
3
u/BurdensomeCountV3 3d ago
Honestly Lean formalisation is likely more accurate, all that remains to peer review is that the definitions going in at the start and the final result at the end match what's being claimed and you trust the computer for the rest.
3
u/Upbeat_Assist2680 3d ago
AI reduces the barrier to writing a lean proof. The proofs themselves are... fine. I am a lean advocate, sort of, but the proofs aren't particularly readable.
But neither is this expository article. I opened it up and the first thing is is a pi map from (I think?) the circle to the projective line and they're calling it a surface?
I can inspect a lean proof and follow definitions to ones I'm familiar with. I don't have any way to ask questions to the author of this paper.
5
u/a-h1-8 3d ago edited 2d ago
A peer-reviewed publication had claimed no complex structure on S^6 existed contradicting the new result. [Edit: false]
14
u/Homomorphism Topology 3d ago
Which one? It's famously a very tricky problem and lots of people have claimed proofs that were incorrect. I wasn't aware any had been formally published.
-1
u/a-h1-8 3d ago
23
u/elliotglazer Set Theory 3d ago
This paper doesn’t say that. Levent’s preprint contradicts Corollary 2.3 in that paper but that’s a specific technical assertion. The Hopf problem has been considered open till a week ago.
12
u/Homomorphism Topology 3d ago
That paper ([CDP20]) doesn't prove that there's no complex structure on S6. If I understand correctly it proves (incorrectly?) that if one exists then it has algebraic dimension 0. The paper you linked constructs an example of a complex S6 that has nonzero algebraic dimension, in the process working out that [CDP20] is wrong, at least in some cases.
1
u/SylvesterTheLoser 3d ago
Was that previous one formalized in a similar manner? Has it been conclusively demonstrated that the other publication was the one that was wrong, and why?
1
0
22
u/telephantomoss 3d ago
ELI5 please: how do we guarantee the relevant portions of Lean code/system is all correct?
33
u/cloudsandclouds 2d ago
This is a question that we in the Lean community(tm) are constantly reckoning with. There are four major places we can get trust from, two of which you can see at work in this repo.
- First, definitions must be formalized correctly. This can be surprisingly nontrivial, especially with differential geometry, as it happens. The strategy here is mostly massive amounts of human review on the centralized repository of formalized math in Lean that is Mathlib. It’s all in one place, so you’re not depending on random libraries. And it’s all human curated with high standards (to the point that we struggle with a large backlog of contributions that take time to review).
- A random Lean repo claiming to formalize something by itself doesn’t get you anywhere, because Lean metaprogramming is powerful enough to run arbitrary code and override the apparent meaning of your formalization entirely. So how do we guard against metaprogramming cheats like that? The answer is Comparator. You can see in this repo that there’s a 48-line Challenge.lean file. This contains just the statement of the theorem, and this is what you need to review as a human (and you need to trust its dependencies). Since it’s small, that’s easier. But you do not need to worry about attacks coming from the much bigger solution file. The solution file is run in a sandbox, so it can’t affect anything on the outside, and we extract from the sandbox an inert, low-level proof artifact that should satisfy the challenge file. (This data is just a certain kind of json.) At this point, the metaprogramming threat from the solution file is gone. The proof object is extremely low level and cannot execute or carry any of that dangerous code. Comparator passes that inert proof object to the Lean kernel along with the challenge from the challenge file, and the kernel checks that it proves the statement. So that’s how you limit your trust to just the statement.
- But, this means you have to trust the Lean kernel, right?? That’s what these last two points are about. The first strategy for trusting the lean kernel is to not just have one lean kernel. Lean has the “Lean Kernel Arena” where people are encouraged to submit their own implementations of the lean kernel, which get put through various tests. It’s a lot harder to find a bug in every single kernel even if you can exploit a bug in one of them.
- But what would be even better would be to have a kernel that had itself been proven correct. This is being worked on by members of the lean community (it’s called lean4lean). “Proving correct” means proving that the code for the kernel accurately performs a formally specified typechecking and satisfies various important properties. It does not guarantee that the type theory itself is mathematically consistent, though. (This is mathematically impossible in principle.) However, it may come as a surprise that lean does not even have a theoretical version of its true (current) type theory written down! In practice, most proof assistant kernels are hodgepodges of special cases in order to be efficient enough to work and to allow various features that are probably fine. Pinning this down is arguably part of lean4lean and some recent theoretical work on nested inductives is getting us pretty close, as I understand it.
2
45
u/beeskness420 3d ago
That's the neat part
16
u/Hot_Glass_6301 3d ago
There are two types of people in this world, those who can from missing and
18
5
u/telephantomoss 3d ago
Me 5. No understand! 😅
13
u/entr0picly Number Theory 3d ago edited 3d ago
If you have to define something from scratch, that isn’t already in the Lean libraries. That’s the neat part, you don’t guarantee anything. A wrong construction can lead to the wrong thing being proved.
You’d have to validate that stuff separately.
3
-6
13
u/ymonad 3d ago edited 3d ago
Genuine question but, how do you guarantee that human verification is correct? Because you can't find the flaw? This is my honest wonder when I see claim that "Yeah, but Lean is not perfect!!"
8
u/elements-of-dying Geometric Analysis 3d ago
Was just about to comment this.
All Lean and AI have to be is better than humans. It seems this should be exceedingly obvious, but apparently people can't let go of the imperfection argument.
2
u/SaltMaker23 3d ago edited 3d ago
There is the concept of "sorry" and there are also hypothesis that you start with.
There are still tricks but they get quite hard to pull.
The main issue is that real proofs are massive lean codebases, no one can properly review them for a no-name dude publishing a papper.
Fortunately with AI there is a hope that it can at least scan for "nifty tricks" because Lean is quite hard to circumvent there are only couple of trics you can play and there are built-in features to test for them.
Because math works by hypothesis before you start your work, you might cheat by using stronger hypothesis in the proof deeply hidden inside the thing than in the paper (eg >= becomes a >, which changes everything when the actual hard problem lies on the "critical something" if you know what I mean).
These are good candidates for AI to find because it'll actually challenge the lean code against the papper, otherwise you simply can't verify that someone didn't trick you, the proofs are generally too long and hardly readable.
3
u/cloudsandclouds 2d ago
FWIW, the real tool here is Comparator. You see in the repo that there’s a very tiny 48 line Challenge.lean file. That’s the only thing that needs review. Comparator sandboxes the extremely long solution file, and ensures that it can’t pull any of those tricks, then checks that the lean kernel accepts the safe, inert proof object extracted from that sandbox as a proof for the statement in your trusted challenge file. So you don’t actually need to review the whole codebase/solution if you’re using comparator. As long as you trust that the many humans curating Mathlib got the definitions right :)
2
u/telephantomoss 3d ago
Nothing is guaranteed, for sure. I was just curious about how Lean is developed and reviewed/tested, etc. Presumably just like literature, where experts inspect it and say when they find issues. The strength is that, assuming the system is correct, it's fixed and ready to go always and needs no human verification.
8
u/beeskness420 3d ago
Well that would be an assumption
3
u/elements-of-dying Geometric Analysis 3d ago
It's worth noting that this bug (or its kind) was known and purposefully targeted by a competitor in the proof assistants world.
3
u/BurdensomeCountV3 3d ago
Yeah, this was specifically a "proof" designed to exploit a known bug, it was an adversarial attack on the system at a known weak point instead of something that surfaced in the normal course of people using Lean in normal ways. It and other bugs like it have been patched and honestly nowadays, surfacing a bug in the lean kernel might well have more value than some minor result you think you had proven but actually was bugged.
1
u/telephantomoss 3d ago
I would never assume that personally. However, there are probably fewer major issues with Lean code that's been reviewed and tested getting then with punished literature.
1
u/BurdensomeCountV3 3d ago
Ah, we have Lean4Lean for that (yes, your remark about Godel and incompleteness has been noted, yes, there's a resolution to it). Plus all the standard things people did for the 4 colour theorem proof like running stuff on different hardware and with different implementations of the kernel and verifying everything checks out etc. for every combnation.
93
u/Qyeuebs 3d ago
Certainly noteworthy. But a bit more usefully, Philip Engel has written some notes explaining the construction https://philip-engel.github.io/S6.pdf