Mathematicians welcome computer-assisted proof in ‘grand unification’ theory
nature.comI recommend the following post, by the author of the proof, for deeper context. Especially near the end, they talk about some of the things they're trying to accomplish with it in plain(ish) English.
https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...
See also [1] for a follow-up blogpost that is less technical.
[1]: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
"Proof assistants can’t read a maths textbook, they need continuous input from humans, and they can’t decide whether a mathematical statement is interesting or profound — only whether it is correct, Buzzard says. Still, computers might soon be able to point out consequences of the known facts that mathematicians had failed to notice, he adds."
I agree, but I think my statement is accurate today in 2021. I would love to see funds directed towards this sort of question. The big problem is that at high level so so much is skipped over, and you still sometimes have to struggle to put undergraduate-level mathematics into Lean -- this is why UG maths is such a good test case.
Very nice to see you here Kevin. We never interacted but I do still remember a lecture you gave at Imperial in '06 where you filled in for Prof. Liebeck and started with Lemma 1: "I am not Professor Liebeck" ;-) Thank you for the nice memory and your important work on / with Lean.
Did he prove the lemma or did he leave it as an exercise :-) ?
> The big problem is that at high level so so much is skipped over
This is an issue, but there's an established practice of writing formal sketches where the gaps in the proof are explicitly marked, and future tooling might bring ways to address these gaps once a full formal context is provided.
One issue is that Lean has little or no support for declarative proof, which is by far the most natural setting for these "proof sketches", and also brings other advantages wrt. complex proofs. (Coq has the same issue; some code was written to support declarative proofs, but it was too buggy and bitrotted, so it got removed.)
As far as I can tell, this is not quite true. Tactic proofs aside, you can also write functional term mode proofs and declarative "structured" proofs in the sense of Isar. Theorem Proving in Lean introduces that style, so most people who use Lean are familiar with it: E.g. https://leanprover.github.io/theorem_proving_in_lean/proposi...
Additionally, even in tactic proofs you can use tactics like `have`, `suffices`, etc. to manipulate the structure of the proof and make subgoals explicit like you would usually do in the structured style. In practice, people in Lean still prefer imperative tactic proofs with the option to write in a structured/declarative style where reasonable. The full "structured" mode does not see much use, since it is quite verbose. As a result, Lean 4 will not support this style out of the box anymore, but you could still add it yourself using the macro system.
It's worth noting that GPT-f already gets a big performance boost from pretraining on Arxiv etc (https://arxiv.org/pdf/2009.03393.pdf#page=7) despite those sources containing next to no Metamath or anything that looks like a raw Metamath proof, just regular natural language & LaTeX discussing math...
How well does text extraction from a PDF work? I almost never try it but thought there were random spaces in the output and such things.
A fair summary would be "often very well, but not always". A good exmaple would be the S2ORC dataset [0]: a dataset of full parses of scientific PDFs. In their paper, the authors write about the difficulties of getting the parsers to work reliably, and how having multiple published versions of a PDF was helpful for when the PDF parser fails on the first one.
It's worth noting that for most papers, arXiv provides the LaTeX source for download, which is presumably what they trained on.
> we're closer to this than people realize
At least give a proper reference to what you're alluding to, please.
Also, closeness in AI has shown to be a misleading concept.
A reference you might like to note is in a response - that kevinblizzard bloke probably has a fair old handle on this stuff. Note how he is quoted throughout the article.
This is about some pretty creative uses of computing in maths and bugger all to do with AI (whatever that is.)
If you put enough blood, sweat and tears into codifying mathematical concepts into Lean, you can feed it a mathematical thingie and it can tell you if that thingie is correct within its domain of knowledge. If you get an "out of cheese error", you need to feed it more knowledge or give up and take up tiddlywinks.
This explains Lean in terms I can understand: https://www.quantamagazine.org/building-the-mathematical-lib...
Simply having a linked graph of related concepts might show "impact diffs" in theorems.
I recall that the Fermat's proof linked several normally disparate areas to get to the meat of the issue.
Simply tagging those relations to identified sub-fields of study will probably help give guidance to impacts of theories, maybe farm them out to advanced students for quick review.
Why do you say this?
I'm not quite sure what you're asking about. I'm saying that we can't yet take the Wiles and Taylor-Wiles proof of Fermat's Last Theorem, feed it into a machine, and get a Lean proof of Fermat's Last Theorem.
I think the GP might have been responding to the GGP, not to your statement in the article.
I remember asking Bob Solovay whether he thought Wiles' proof of FLT was within reach of formalization and he said something like: it is probably 20 years away. It may have been 20 years since I asked him that, and seeing this recent work with Lean makes me think FLT might also be doable, which would make Solovay's guess just about spot on.
Hi Kevin,
Yes, I was responding to the person who said “we're closer to this than people realize” hoping to learn what they had in mind.
Can't usefulness be approximated like Google search results of old, by connectedness to other theories.
This is going to be an exciting area.
I spent some time previously playing with Coq. It's very powerful, but even proving the simplest undergraduate maths statements (say, about group theory) can prove very challenging. I believe that part of this is that Coq uses different mathematical foundations than traditional mathematics, which mostly uses set theory (ZFC, although most people don't care about the specifics). So it can be hard or unnatural to express something like "subgroup". I don't know if Lean fares better in that respect. Coq documentation is also IMHO almost impossible to understand unless you're already very deeply knowledgeable about the system.
We will probably still need some more iterations, to get more user friendly assistants with better documentation and to get adequate teaching resources etc.
In my experience, the difficulty is very rarely the transition from set theory to type theory. I find this almost transparent in practice.
The issue is rather that you need to deal with edge cases that are usually swept under the rug, or that you need to spend a full page working out the details of a proof that everyone recognizes as obvious. It would be great if computers could give even more assistance with these tedious parts of formalization, and I'm very glad that people are working hard on realizing this.
One area I've been playing with is "theory exploration", which takes a set of definitions and produces lemmas that are 'interesting' (i.e. irreducible, via some scheme like Knuth-Bendix rewriting).
(Thanks to Curry-Howard, we can also view this as generating test suites/specifications for software libraries!)
Notable tools include Hipster, IsaScheme, IsaCoSy, QuickSpec and Speculate.
Kurt Gödel with a bat in dark alleyway of obviousness haunts my dreams.
Here's the definition of a subgroup in Lean's mathlib: https://leanprover-community.github.io/mathlib_docs/group_th...
Given a group G, there is a type `subgroup G` of subgroups of G, and a subgroup is a structure consisting of a set of elements of G along with some proofs that it has the identity, it's closed under multiplication, and it's closed under taking inverses. Lean has a coercion facility using typeclasses, and there is a typeclass instance that will use the subgroup's set coerced to a type when the subgroup is used in a place that expects a type. This coerced type has a group typeclass instance, so a subgroup "is" a group.
The big complexity in all of this doesn't seem to be ZFC vs type theory, but rather how do you implement a mathematician's use of synecdoche and implicit coercions. Synecdoche is the figure of speech where you refer to a thing by its parts or vice versa -- for example, "let G be a group" and then using G as if it were a set, even though a group consists of a set, a binary operation on the set, a choice of identity element, and a few axioms that must hold. Mathlib uses typeclasses to implement the synecdoche -- a type is a group if there is a typeclass instance that provides the rest of the structure. As I understand it, Coq's Mathematical Components library uses structures and unification hints instead (though I've failed to understand how it works exactly), but I have heard that they can be very fiddly to get right.
I think you'd have to find solutions to these same problems no matter the foundations. At least with types, there's enough information lying around that, for example, group structures can be automatically synthesized by the typeclass resolution system in many common situations.
Lean's foundations are similar to Coq. I think the ergonomics are a bit better.
Most activity in proof systems is based in type theory these days, but set theoretical systems do exist, of which Metamath is the most mature. That said, Metamath is seriously lacking in automation, so there is an element of tedium involved. That's not because of any fundamental limitations, but I think mostly because people working in the space are more motivated to do things aligned with programming language theory. There was also a talk by John Harrison a few years ago proposing a fusion of HOL and set theory, but I'm not sure there's been much motion since then.
I believe a fully featured proof assistant based in set theory would be a great contribution.
It depends on what you mean by "fully featured" but Isabelle supports ZF logic [1] and also you can do ZFC in Isabelle/HOL [2]. And, of course there is Mizar [3].
[1] https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html
Hey type hacking is hard. Agda is kinda easier for someone who knows haskell, but hard nonetheless.
You don't need subgroups, you just need injective homomorphisms.
That's a nice idea but it tends to fall flat when you can't actually construct an explicit function exhibiting the homomorphism in question (which does happen from time to time). A lot of equivalences in areas like group theory only hold classically.
Your concerns make sense in general, but I have hard time understanding them for would-be subgroups. I would think the "explicit function" would be the easy part. The hard pat is annoyance of finding a "syntactic" representation of the subgroup and proving it's a group (closed) in its own right.
In any event, Lean's reputation is that it goes the extra mile for "regular" mathematicians. It probably has something nicer for this just like it does for quotiented types.
Nope, proving something is a group doesn't usually run into foundational concerns (at least if you use setoid equality). But finding a function exhibiting a homomorphism can unless you use a functional relation instead (but then you lose most of the nice benefits of using this version of the definition in the first place).
ZFC was only ever developed as a proof of concept, not as a practical foundation for formal math. Structural set theories, type theories or category-based foundations are actually a lot easier to work with, and otherwise quite equivalent in power.
This is missing the point. Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. It requires a lot of effort to reformulate all of mathematics into equivalent formulations. That makes it harder to get buy-in from many working mathematicians, and it also makes the subject less approachable for, say, undergraduates.
> Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations.
Yes, but only the foundations. A math undergrad doesn't actually care whether an ordered pair (a, b) is encoded as {{a},{a,b}} or as an instance of the product type, and they don't care whether the natural number 2 is encoded as the set {{},{{}}} or as a value S(S(Z)) of the inductive type of the natural numbers. Although if pressured to choose, I bet they'd prefer the latter, since it gets a lot closer to how everyone thinks of "ordered pairs" and "natural numbers".
Since mathematicians always work with higher-level abstractions anyway, I don't think the fact that the very lowest layer of these abstractions is set theory actually gets in the way of formalization efforts.
Modern math textbooks are based on naïve set theory, which can be quite feasibly modeled, even by structural foundations. It might require some effort at the lowest layer of formalization, but even then only as a one-time thing that's not going to impact the project as a whole.
That may very well be the case, but to a person starting out right now, those foundations seem to be lacking right now (or at least are not easily discoverable).
Not quite. You're conflating two things: using set theory to talk about sets (what undergraduate math textbooks do) and using set theory to talk about everything (what ZFC foundations does).
In 99% of algebra textbooks you'll see a definition like "if G is a group and H is a subset of G, then we call H a subgroup if it is a group under the same operation." Then, the next thing you see is probably the theorem that "H is a subgroup of G if and only if it is a subset of G and gh^{-1} € H for all g, h € H". That's clearly using the language of set theory to talk about groups.
I mean, my argument is not that type theory or anything is unsuitable for doing maths. It's that it is different from how most people do maths. In my particular case, I am such an undergraduate who has actually tried to do some group theory in Coq and found it annoying to pull it off—not in the least because I figured out there were multiple equivalent ways of e.g. defining what is a group and/or subgroup and I had no idea which one was more natural or useful; you can work with injective homomorphisms, as someone else suggested, but you can also work with predicates so that you define a subgroup as all elements of some type that satisfy that predicate. Moreover, the fact that Coq includes several different types of "truth" (basically, Bool vs. Prop), which is undoubtedly well-reasoned, requires some adjustment, too.
Again, I'm not saying that this is a failure of tools such as Coq (although, they should really make documentation more discoverable and understandable). My sole argument was that you can't currently take any mathematician not particularly interested in logic or proof theory, especially not an undergraduate student, and expect them to encode simple proofs that they understand in Coq without a lot of assistance. If these tools are to be the future of (some part of) mathematics, they will have to become more accessible one way or another.
Ironically (?), I found that it was much easier to use Coq to prove e.g. algorithms correct (especially if you've done functional programming before) because programming languages actually do use types (even if some of them only do so at runtime).
> That's clearly using the language of set theory to talk about groups.
If you like the language of set theory, what's wrong with replacing "A ⊆ X" with "A : SubsetOf X" where SubsetOf X = X → Prop? This is what Lean does: https://leanprover-community.github.io/mathlib_docs/group_th...
> there were multiple equivalent ways of e.g. defining what is a group and/or subgroup
Don't you have that problem in any foundation?
> Moreover, the fact that Coq includes several different types of "truth"
You probably know this already, but you can collapse Prop to Bool by adding some classical axioms.
> My sole argument was that you can't currently take any mathematician not particularly interested in logic or proof theory, especially not an undergraduate student, and expect them to encode simple proofs that they understand in Coq without a lot of assistance.
True, but I don't think that's a goal of the Coq developers right now. I feel like Lean is the only project trying to make formal proofs of classical mathematics accessible to an undergraduate student.
> My sole argument was that you can't currently take any mathematician not particularly interested in logic or proof theory, especially not an undergraduate student, and expect them to encode simple proofs that they understand in Coq without a lot of assistance.
Oh but absolutely, I agree 100%. I consider it the "holy grail" of interactive proof assistants: an assistant that understands mathematics as written by humans in papers, plus is capable of filling in intuitively trivial/boring steps. In other words: an assistant that is usable by someone with training in mathematics but not necessarily requiring training in the tool itself.
A quick intro from quanta magazine to Kevin Buzzard's work on computer-assisted proof systems
i love the time that we live in. people talk about there being a glut of podcasts, but i can type "Peter Scholze" into youtube and there is a full hour-long interview with him hosted by another mathematician. you can see her channel is very new and almost certainly a part of this latest wave of pandemic podcasters. its so great to take an interest in a random person from a nature article and be able to immediately get a visceral idea of who he is and what hes about.
For anyone frustrated that the article doesn’t say what specific part of math has the most to gain it’s here:
“ The crucial point of condensed mathematics, according to Scholze and Clausen, is to redefine the concept of topology, one of the cornerstones of modern maths. A lot of the objects that mathematicians study have a topology — a type of structure that determines which of the object’s parts are close together and which aren’t. Topology provides a notion of shape, but one that is more malleable than those of familiar, school-level geometry: in topology, any transformation that does not tear an object apart is admissible. For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line.
Topology plays a crucial part not only in geometry, but also in functional analysis, the study of functions. Functions typically ‘live’ in spaces with an infinite number of dimensions (such as wavefunctions, which are foundational to quantum mechanics). It is also important for number systems called p-adic numbers, which have an exotic, ‘fractal’ topology.”
I know nothing about topology. If you have time, could you please explain this sentence?
"For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line."
Is it because triangles and circles are "2D" and lines aren't?
Crudely speaking, topologists consider spaces as if they're made of rubber - a mathematically perfect rubber that can be made infinitely thin or stretch to infinity. So, a circle can be made with an infinitely thin circular rubber ring, and you just pinch three points and stretch, and you get your triangle, in any shape.
But you can't get a straight line - to do that you need scissors to cut one point of a circle (to be precise, remove a single point) - and then you can stretch the remainder to infinity and now you have your line.
You can give a function that maps the points of the triangle to the points of the circle in such a way that this function is continuous. (Continuous basically means "no jumps".)
You can give this function explicitly. Let's assume that the triangle is drawn on a piece of paper with an x and y axis, such that the intersection of the axes (the origin) is inside the triangle. For each point on the triangle, draw a line from the origin to the point. Take the angle between that line and the x-axis. Use that angle to map it onto a circle.
If you remove a point from a line, it breaks into two pieces.
No. Both are 1-d (lines).
It's because triangles are loops (closed) and straight lines aren't.
For more details about the actual proof, see: 'Blueprint for the Liquid Tensor Experiment'
This kinda gives me chills because I can't help but think of Warhammer 40k.
Essentially our civilization progressed to the point where computers started to take more of a role in new discoveries much like in the real world. As computers got more powerfull and AI developed naturally scientific advancement sped up. But there came a point when the science and math became too advanced for humans to even comprehend, so computers did it. Then there came a point when things were so advanced that even scientists couldn't even ask the right questions so an AI intermediate would have to be used.
Then things get weird and you have the 40k universe.
Anyways I know I probably butchered it a little but that's the gist of it and I can totally see things progressing in the real world up to the point where things get weird in 40k.
The abiltiy to automate proofs creates some interesting questions about the nature of mathematics. The article remined me of Erdos saying that you "don't need to believe in God, but you do need to believe in the book", 'the book' here being an imagined collection of mathematical proofs that are so simple, clear and beautiful that they immedieately stand out to any mathematician.
I don't mind proof assistants as a way to gain new insights into mathematics, but I worry that maths is drifting into a direction where it turns more into hermeneutics than actual mathematics. The automation of proofs isn't the only thing, I also was very scpetical about the whole process of Shinichi Mochizuki's proof of the abc conjecture.
As explained in another comment, there is only very mild proof automation going on in this Lean project. Every non-trivial idea has to be supplied to the computer by a human being.
The whole circus around Mochizuki's proof of the abc conjecture was dealt with quite well by the social structure of the mathematical community. Many people looked at the proof. Many people got stuck. Several experts got stuck at exactly the same point. And Mochizuki refuses to acknowledge that there is a problem at that point of his "proof". But a consensus was reached in the mathematical community (maybe minus RIMS).
What's the name of this point? It's really hard to find any progress on this topic regarding Mochizuki other than some popular articles without any content.
See https://www.math.columbia.edu/~woit/wordpress/?p=10560, which links to a technical write-up by Scholze and Stix about what they think is the issue with Mochizuki's proof. Woit's blogpost also gives a bit more links, including a response by Mochizuki.
The paper which everyone linked to when the discussion was going on now 404s, so here is a new link: https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
The point in the proof where scholze and stix show it fails is “IUTT-3, Corollary 3.12”
Made an account just to share this incredible book that follows Erdos's life & exploits:
https://en.wikipedia.org/wiki/The_Man_Who_Loved_Only_Numbers
On the contrary proof assistants help one systematize and organize existing concepts. They are a great way to revise the basic curriculum and revolutize pedagogy. They make the creative process of defining new mathematical objects more accessible, and easier to motivate via unlocking more code reuse. They are a great way to revise the basic curriculum and revolutize pedagogy.
I strongly agree on this one. As a programmer and someone who's always been interested in mathematics, having a way to check proofs without relying on trust of my own logic or a third agent, but solely on a prover like Lean or Coq is a really big difference.
Automated proofs aren't remotely comparable to Mochizuki's abc stuff. Automated proofs just handle a lot of complicated case by case checking that humans could in principle do, it's just too much work, like counting to a trillion. Automated proof systems are incapable of the brilliant but unreliable intuitive leaps that mathematicians can make.
Mochizuki's stuff is simply a hypercomplicated pile of nonsense unintelligible to the mathematical community.
> Automated proof systems are incapable of the brilliant but unreliable intuitive leaps that mathematicians can make.
I would add current automated proof systems. IMHO we are just at the beginning that mathematicians realize the usefulness of technology, which was basically neglected ever since.
It will be very interesting to see what happens! A common theme in mathematics is that the proofs are the (relatively) easy part, while knowing what to prove is hard. Still, I'm sure mathematicians will welcome greater automation of the "easy" part. If machines ever do more than drudge work, there will also be the challenge of making the machine-generated proofs intelligible to humans, similar to the interpretability issues around machine learning models today.
> but I worry that maths is drifting into a direction where it turns more into hermeneutics than actual mathematics
Related to the unexplainability of AI. We're just grasping for more than we can hold in our little working memory.
> But systems known as proof assistants go deeper. The user enters statements into the system to teach it the definition of a mathematical concept — an object — based on simpler objects that the machine already knows about. A statement can also just refer to known objects, and the proof assistant will answer whether the fact is ‘obviously’ true or false based on its current knowledge.
As far as I can see this is just programming. How is this different from writing in Java
int i = “hello”
Of course, we need more complex types than “int” and “String”, but in principle it’s the same.
Yeah you can say that. You can also say that Machine Learning is just programming. Or in a similar way you can also say that First Order Logic is just programming.
However, the cool thing about programming is that it lets us represent a lot of different things. In this case you're representing the construction and interaction of mathematical objects, with a language that targets a specific proof management system to verify this constructions.
But yes, it is "just programming", and some functional languages even support proofs to some extent like Scala or Agda.
Yes and the isomorphism is known as Curry-Howard Correspondence https://en.wikipedia.org/wiki/Curry-Howard_correspondence
Does anyone know how condensed mathematics would fit into the modern theory of PDEs (which is heavily based on functional analysis)? Perhaps it's a relic of the sort of math Scholze works on, but it looks far too abstract to provide an impetus for people in those fields to embrace it. Topology, on the other hand, is relatively easy to define and work with (though there are some quirks with dual spaces of continuous linear functionals I've seen aesthetic objections to). Or does it "contain" topology in some sense, allowing people to continue working with notions of convergence obtained from norms?
I think that right now it is not clear why condensed/liquid mathematics would be useful for PDEs. On the other hand, your question
> Or does it "contain" topology in some sense, allowing people to continue working with notions of convergence obtained from norms?
has a positive answer. You can, if you want, swap out topological spaces, and use condensed sets instead, and just continue with life as usual.
At the same time, all of this is in fast paced development, so hopefully we will see some killer apps in the near future. But I expect them more in the direction of Hodge theory and complex analytic geometry.
Thanks for sharing your expertise. Would you be open to sharing your background? Obviously it's not required, but it would help contextualize what you're saying for the interested non-mathematician; otherwise we're kinda stuck with 'some guy on the Internet said ...' syndrome. :)
Sure, I just created an account a couple of days ago, and my favourite username was already taken :oops:
I'm Johan Commelin, https://math.commelin.net/
Hi! Imagine for a moment that your next project required you to develop a lot of functional analysis and PDE theory in Lean. Would you be tempted to build that on top of what you've done (or will have done) with condensed sets?
Right now, I think I would go for that classical approach, simply because there is more supporting material for that in the library, and there are more people who understand that approach and can help contributing. (I'm talking specifically about functional analysis and PDEs here.)
On the other hand, it should be a lot of fun to see if we can formalize the new proof by Clausen--Scholze of Serre duality. Using their machinery, the proof should simplify a lot. But this requires building complex analytic manifolds on top of condensed mathematics. So we would first need to set up those foundations.
Thank you! And welcome! Make yourself at home.
clicked on the private key link; haven't laughed this much in days
Interesting choice of the proof assistant though - some specific parts of the Lean's core are not completely decidable, moreover the upcoming Lean 4 version is incompatible with many libraries and proofs written for Lean 3. See also the discussion[1] if the Coq is suitable for number theory as quotients are ubiquitous here.
The claim that Lean's core is not completely sound is FUD. Completely bogus.
You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `false` so far in Lean 3.
The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substantial user base of mathematicians somewhat familiar with the subject at hand (i.e., condensed mathematics).
The initial challenge by Peter Scholze was directed at all theorem proving communities. As far as I know, only the Lean community took up the challenge.
(Concerning Lean 4: yes, mathlib will have to be ported. And yes, people are working hard on this. I think that none of the theorem provers so far are ready for wide-scale use in mathematics. And that's why it is important to iterate fast. The Lean community is not afraid of redesigns and large refactors when discovering better approaches.)
> You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `false` so far in Lean 3.
You are right, my bad. Taking my words back on that.
A bit more details from the Pierre-Marie Pédrot:
> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around.
> The first thing they do is to axiomatize quotient types, which is somewhat fine and can be done the same in Coq. As any use of axioms, this breaks canonicity, meaning your computations may get stuck on some opaque term. (While slightly cumbersome, axiomatizing quotients already solves 99,9% of the problems of the working mathematician).
> Now, were they do evil things that would make decent type theorists shake in terror, they add a definitional reduction rule over the quotient induction principle. We could do the same in the Coq kernel, but there is a very good reason not to do this. Namely, this definitional rule breaks subject reduction, which is a property deemed more important than loss of canonicity.
> In Lean, you can write a term t : A where t reduces to u, but u doesn't have type A (or equivalently may not typecheck at all). This is BAD for a flurry of reasons, mark my words. Reinstating it while keeping quotients requires an undecidable type checking algorithm, which is another can of worms you don't want to wander into. The same kind of trouble arises from similar Lean extensions like choice.
> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around.
This is not the first time that I hear someone from the Coq community talk about Lean and its "mastermind PR campaign". To me it comes across in a denigrating way, and frankly I'm a bit sick of it.
Working mathematicians are usually not experts of type theory. Yes. But they aren't stupid either. Why does the Lean community have such a large number of mathematician users? Why did it successfully formalize the main technical result of Peter Scholze's challenge in less than 6 months? Is this all because of a "mastermind PR campaign" selling mathematicians snake oil?
There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on.
I'm fine with people finding the foundations of Lean ugly, distasteful, improper, or whatever. But please stop the insults.
The context of that "mastermind PR campaign" comment is a video watched now more than 70,000 times in which it's claimed that Coq is just not as good as Lean because it doesn't have quotient types, even though you can get them if you're willing to make the same trade-off that Lean does (broken SR). Calling Lean's framing a 'mastermind PR campaign' is of course still quite snippy, but I don't think it's totally unfair seeing as how it led to those comments.
>There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on.
I think it just takes time to fully move on. And while it's not the fault of the Lean community, when something like the recent quantamagazine article on formalizing mathematics essentially only mentions Coq to call it old and busted in comparison to Lean, that's only going to cause people to hold onto their resentments for longer.
The Coq folks tend to focus on constructivity, and Lean gets sold as a constructive system but then you get this weird axiomatised-quotients stuff that's the farthest thing from constructivity. I can see how they might find that kind of thing highly frustrating.
It might not show up as a problem if you only ever care about classical stuff, but there are arguably better ways of doing purely classical mathematics that don't arbitrarily break interoperability w/ the constructive world.
Where does Lean get sold as a constructive system? Certainly mathlib (the main maths library in Lean) is very upfront about being classical.
mathlib != Lean. I'm talking about the basic logic. People will try to sell you Lean by describing its system as constructive, but if so the quotients stuff is pure breakage as the Coq folks point out.
And if Lean could support classical logic without arbitrarily breaking interop for folks who want to also prove constructive statements, we might see some additions to mathlib with a closer focus on constructive math.
I agree very much that mathlib != Lean. Still, I think much of the talk about Lean will mention that mathlib is classical.
It was an honest question: I don't know where Lean is sold as a constructive system. (Note, I haven't read every part of Lean's documentation or website. I might be missing something obvious here.)
I don't think anyone is trying to sell Lean as a constructive system. The current developers certainly don't think of it that way, further evidenced by the fact that the typical way of doing computation in Lean does not involve definitional reduction, but using `#eval` with additional low level code for performance. Proof irrelevance (and quotients) were adopted with that in mind.
You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think
Some constructivists may also take offense with proof irrelevance (and the resulting loss of normalization [1] or its incompatibility with HoTT), which you can only really avoid by avoiding Prop.
There is also a problem of HoTT and equality reflection incompatibility[1].
[1] https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr...
Ok, no worries. I understand that from a theoretical point it's not so nice that defeq is not decidable. But frankly I don't care. Because in practice, I don't know of any example where someone was bitten by this. It only shows up in contrived examples. And even if you have some practical example where lean gets stuck on A = B, it will probably be very easy to find a C so that lean gets unstuck on A = C = B.
[Edit, this comment only replies to the first paragraph of parent. I wrote it before parent was edited.]
By the way, just for the record, I like many aspects of the new Lean 4 design and wish the project luck. They really aim for better maintainability and user experience. It is nice to see them taking best solutions from other programming languages and frameworks.
I haven't used quotients (or Lean), but I've certainly encountered subject reduction problems in Coq when using coinduction, so this sounds a tad hypocritical.
It's certainly good to avoid breaking subject reduction even more though ;)
Pierre Pedrot has been very vocal in his belief that broken SR from coinductive types is a serious problem with Coq that needs to be fixed. This is quite different from introducing stuff that deliberately breaks it.
There's ongoing work[1] on fixing that. Also let's see how migrating setoids to cubical type theory might fix more issues for Coq. Will they follow the Arend[2] path? That remains to be seen.
Shouldn't it be easy to automatically port theorems? If they are well defined there can't be ambiguity
Yes and no. If you want to port large low-level proof objects in all their gory detail, then this has been done already. But if you want to port the more concise higher-level proof scripts you run in all the same issues as with regular transpilers.
Compare it to porting machine code for one instruction set to another instruction set. This is usually doable in a straightforward manner (maybe with a mild performance penalty). But transpiling idiomatic Java to idiomatic Haskell is nigh impossible.
Luckily, the differences between Lean 3 and Lean 4 are not as large as between Java and Haskell. But still, they have different idioms, different syntax, different features. And this has to be taken care of.
In theory yes, but there are two main things that makes it harder :
- some technical details have changed. They don't affect the axiomatic aspects of Lean, but they force us to redefine some things in a cleaner way.
- we don't only want to port the theorem. We want to port them to a human-readable proof that can be easily maintained
As to decidability: I suspect you mean that Lean's foundations are non-constructive. I'd rather they weren't, but with what Peter Scholze is doing, I'd be surprised if the arguments could be made constructive within just a few years from their conception. This usually takes much longer (e.g., constructive proofs of the Quillen-Suslin theorem appeared in print just a few years ago).
About incompatibility: Last time I checked (some 3 or so years ago), Coq was not backwards compatible either, and libraries had to be ported manually with each update. Sadly, as this is the one greatest anti-feature that is currently putting me off proof assistants, but probably it needs some time, and the quickest way to get there is to maximize usage. From what I know about Coq and Lean, I suspect Lean will stabilize faster than Coq does, due to it being more "declarative" (Coq is based too much on complex tactics, which are hard to make stable by design).
I wasn't aware of Lean not being sound and a quick search didn't come up with anything related to that. Could you link a source?
See other comment. It's sound but not decidable.
Basically it turned out that theoretical undecidability did not matter in practice, because Scholze mathematics relies so little on definitional equality. We prove theorems with `simp` not `refl`. Pierre-Marie Pédrot is quoted above as saying that various design decisions are "breaking everything around", but we don't care that our `refl` is slightly broken because it is regarded as quite a low-level tool for the tasks (eg proving theorems of Clausen and Scholze) that we are actually interested in, and I believe our interests contrast quite a lot with the things that Pédrot is interested in.
And in "Lean style", refl proofs are a bit distasteful from a software engineering point of view because they pierce through the API of a mathematical object. (In the language of OOP, it can break encapsulation.)
It tends to be a good idea to give some definition, then prove a bunch of lemmas that characterize the object, and finally forget the definition.
Can you explain to a non-mathematician how you can prove anything without refl (which I assume is the statement “x=x is true”) ?
The jargon is a bit confusing sometimes. In Lean, "refl" does a whole lot more than prove x=x. It is of course available if you want to prove x=x, but the real power of "refl" is that it also proves x=y where x and y are definitionally equal. Or at least that's the idea; it turns out that lean's definitional equality relation is not decidable so sometimes it will fail to work even when x and y are defeq, and this is the theoretically distasteful aspect that came up on the linked Coq issue. In practice, the theoretical undecidability issue never happens, however there is a related problem where depending on what is unfolded a proof by "refl" can take seconds to minutes, and if alternative external proof-checkers don't follow exactly the same unfolding heuristics it can turn a seconds long proof into a thousand-year goose chase. By comparison, methods like "simp" have much more controllable performance because they actually produce a proof term, so they tend to be preferable.
Thanks for the explanation. Is the defeq undecidability a bug of Lean that should be fixed in the future? Or is it an intentional design decision for it to function properly for other types of proofs?
Defeq undecidability is a feature of Lean in the sense that it is a conscious design decision. As we have seen both in this thread and in other places, this design decision puts off some people interested in the foundations of type theory from working with Lean. However it turns out that for people interested other kinds of questions (e.g. the mathematics of Scholze), defeq undecidability is of no relevance at all.
Here's an analogue. It's like saying "Goedel proved that maths was undecidable therefore maths is unusable and you shouldn't prove theorems". The point is that Goedel's observation is of no practical relevance to a modern number theorist and does not provide any kind of obstruction in practice to the kind of things that number theorists think about.
I am quite confident that the developers of lean consider it a feature (or at least, not a bug). Though I'm also not sure why they are building on a complex metatheory like CiC if they are willing to accept undecidable typechecking since you can simplify a lot of things if you give that up.
What simplifications do you have in mind?
I think one of the reasons is that Lean's approximation of defeq still works well enough in practice. As mentioned by others, you never really run into the kind of counter examples that break theoretical properties, but instead into examples where checking defeq is inacceptably slow, which remains an issue even when defeq is decidable.
From my understanding CiC is used because it allows using a unified language for proofs, specifications, programs and types, which greatly simplifies the system. For example, in Lean 4, more or less the entire system is built on the same core term language: Proofs, propositions / specifications, programs, tactics (i.e. meta programs), the output of tactics and even Lean 4 itself are all written in that same language, even if they don't always use the same method of computation. In my eyes, for the purposes of writing and checking proofs, CiC is quite complex; but if you want to capture all of the above and have them all checked by the same kernel, CiC seems like a fairly minimal metatheory to do so, even with undecidable type checking.
For example, if you are willing to accept undecidable typechecking, you can define inductive types in a much simpler theory (inductive types and dependent pattern matching are by far the most complex parts of CiC): https://homepage.cs.uiowa.edu/~astump/papers/from-realizabil... .
There are a few other examples but this is the one that immediately sprung to mind. The complexity of CiC is very much about decidable typechecking, it's not fundamental to writing a sound dependently typed proof assistant. And anyone who has actually worked on a kernel for CiC knows that while it is "minimal" compared to what people want to do with it, no efficient kernel is nearly as minimal as something like λP2 with dependent intersections.
Thanks! But does that not already answer your question as to why Lean would use CIC and not a simpler metatheory?
That particular paper is from 2016 and the type theory presented there is still lacking a number of features from CIC, with those particular extensions being listed as further research. Work on Lean started in 2013 and the kernel in particular has not been touched in a long time for good reason. Around that time, CIC was already battle-proven with there being popular and well-tested reference implementations to learn from. Since then, all the fancy work has been done on the system surrounding the kernel.
I believe one of the goals at the start was that the kernel should be sufficiently simple and small so that it is easy to ensure that the kernel is correct. Despite the apparent redundant complexity that you suggest, the implementation still seems to be sufficiently simple to reach this goal, as no proof of false that was a result of a kernel bug has been reported yet. CIC being well-tested surely also contributed to that.
Another reason is that, as I understand it, it was not always obvious that Lean would break decidability of defeq. Afaik proof irrelevance was only baked in with Lean 3, while it was an option before that. By that point I don't see much of a reason to rewrite an entire kernel that has worked fine so far.
I also vaguely remember that there were arguments related to performance in favor of the current system (e.g. versus W-types), but I don't really understand these things well enough to make that point with confidence :)
How are the ergonomics of a proof assistant based on λP2? Lean does a lot of elaboration of metavariables and typeclass instances and such before handing things off for checking by the kernel -- I'm curious about whether λP2's undecidability is decidable enough, so to speak.
That's currently an open research question, but the answer most likely is that the ergonomics could be made just as good, considering that elaboration of metavariables, typeclass instances, etc. already uses possibly-undecidable algorithms distinct from those used in the kernel in just about every proof assistant I'm familiar with (Lean included).
In terms of stuff that do go more or less directly through the kernel, some followup papers to the one I linked discuss how to translate inductive definitions etc. automatically into a form accepted by the simpler kernel, so I am even more confident that this would not present a problem.
The fact remains though that Lean 3 worked well enough to do Scholze level mathematics. I never quite know what to make of people saying "if the designers had done it in some other way, it would have been better". Of course if someone comes along doing it another way, and then they go on to also achieve Scholze level mathematics, then I will be all ears.
That's a very strange line of argument. Many great programs have been written in C. That doesn't mean that there is no way to improve on C. Perhaps to even the playing field, this hypothetical competitor should be given the resources of Microsoft Research as well :)
I think Kevin is asserting that to make strong comparative claims about the quality of either system, it's good to have a large and functionally similar body of work to compare the systems with, not that there is no way to improve on Lean's core :)
MSR funds a single developer. The Lean community consists of at least 30 or so active contributors right now, with many more having contributed in the past. Most folks work in academia. Much of Lean's success is absolutely due to the work of that single developer, but I don't think that the playing field is uneven due to MSR's funding.
The Lean version of the theorem was 10,000s lines of code...
With verifiers like this as a useful tool, I'm guessing in the coming years this LoC will be dwarfed.
I'm a bit surprised a theorem of major complexity reduced to that small a LoC count.
TIL: Fields medallists ask questions on MathOverflow... [1]
This has me in awe about the depth of mathematics, the pace of progress, the miracle of specialisation. I have a degree in an applied-math-y adjacent field, and understand nothing. (And, btw, I was astonished how knowledgable some commenters right here were, and then realised that we have the (co-)authors of the results themselves here! gotta love HN.)
With that said, here some (non-mathematical) snippets I found interesting (apart from the great word "sheafification"):
> Why do I want a formalization?
> — I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. In the end, we were able to get an argument pinned down on paper, but I think nobody else has dared to look at the details of this, and so I still have some small lingering doubts.
> — while I was very happy to see many study groups on condensed mathematics throughout the world, to my knowledge all of them have stopped short of this proof. (Yes, this proof is not much fun…)
> — I have occasionally been able to be very persuasive even with wrong arguments. (Fun fact: In the selection exams for the international math olympiad, twice I got full points for a wrong solution. Later, I once had a full proof of the weight-monodromy conjecture that passed the judgment of some top mathematicians, but then it turned out to contain a fatal mistake.)
> — I think this may be my most important theorem to date. (It does not really have any applications so far, but I’m sure this will change.) Better be sure it’s correct…
> In the end, one formulates Theorem 9.5 which can be proved by induction; it is a statement of the form ∀∃∀∃∀∃ (\forall \exists \forall \exists \forall \exists), and there’s no messing around with the order of the quantifiers. It may well be the most logically involved statement I have ever proved.
> Peter Scholze, 5th December 2020 [2]
Question: What did you learn about the process of formalization?
Answer: I learnt that it can now be possible to take a research paper and just start to explain lemma after lemma to a proof assistant, until you’ve formalized it all! I think this is a landmark achievement.
Question: And about the details of it?
Answer: You know this old joke where a professor gets asked whether some step really is obvious, and then he sits down for half an hour, after which he says “Yes, it is obvious”. It turns out that computers can be like that, too! Sometimes the computer asks you to prove that A=B, and the argument is “That’s obvious — it’s true by definition of A and B.” And then the computer works for quite some time until it confirms. I found that really surprising.
Question: Was the proof in [Analytic][4] found to be correct?
Answer: Yes, up to some usual slight imprecisions.
Question: Were any of these imprecisions severe enough to get you worried about the veracity of the argument?
Answer: One day I was sweating a little bit. Basically, the proof uses a variant of “exactness of complexes” that is on the one hand more precise as it involves a quantitative control of norms of elements, and on the other hand weaker as it is only some kind of pro-exactness of a pro-complex. It was implicitly used that this variant notion behaves sufficiently well, and in particular that many well-known results about exact complexes adapt to this context. There was one subtlety related to quotient norms — that the infimum need not be a minimum (this would likely have been overlooked in an informal verification) — that was causing some unexpected headaches. But the issues were quickly resolved, and required only very minor changes to the argument. Still, this was precisely the kind of oversight I was worried about when I asked for the formal verification.
Question: Were there any other issues?
Answer: There was another issue with the third hypothesis in Lemma 9.6 (and some imprecision around Proposition 8.17); it could quickly be corrected, but again was the kind of thing I was worried about. The proof walks a fine line, so if some argument needs constants that are quite a bit different from what I claimed, it might have collapsed.
Question: Interesting! What else did you learn?
Answer: What actually makes the proof work! When I wrote the blog post half a year ago, I did not understand why the argument worked, and why we had to move from the reals to a certain ring of arithmetic Laurent series. [...]
Question: So, besides the authors of course, who understands the proof now?
Answer: I guess the computer does, as does Johan Commelin. [Note: = deadbeef57 here on HN][3]
[1] https://mathoverflow.net/questions/386796/nonconvexity-and-d...
[2] https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...
[3] https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
is there a simpler version of LEAN suitable for high school student level math? Sympy?
You might enjoy http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game...
It's a game implemented in lean, where you work your way through the basic facts about natural numbers.
sympy is not a proof assistant, but a symbolic computer algebra system
Well I'd say it's enough to automatically solve many high-school level problems, automatically. Like a poor man's Mathematica or WolframAlpha.
Yes, but that's a totally different category of problem from what proof assistants do.
Is there any opportunity for interested undergrads to learn about this more (since I doubt we could contribute)?
If you're interested in interactive theorem proving with Lean (and not condensed mathematics), the Lean community landing page is a good place to start. https://leanprover-community.github.io/
Especially the "Natural Number Game" under "Learning resources" has been successful in teaching folks the very basics for writing proofs. Once finished, a textbook like "Theorem Proving in Lean" can teach the full basics. Feel free to join the Lean Zulip at any point and ask questions at https://leanprover.zulipchat.com/ in the #new members stream.
Mathlib has plenty of contributions from interested undergrads :)
The article is interesting, but that lede is incoherent. Many mathematicians accept computer proofs the way chess grand masters accept computer players. Computer “assistants” that generate proofs that humans cannot follow or understand will always be controversial, and the proofs they generate, even though accepted as valid, will always be decorated with an asterisk.
This is a proof assistant, not an automated theorem prover. The user has to supply* the mathematics and the proof checker formally verifies whether or not the steps are correct. It doesn’t have any creativity (that’s up to the mathematician).
*I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supplied by the user.
That's not quite true. Many of these proof assistants support some level of automation and proof search. I haven't used Lean specifically, but it's quite common in Coq for projects to write proof search techniques specific to the problem domain and utilize them in their proofs.
True, and Isabelle can call out to automated provers (a mechanism called "sledgehammer"!)
Thanks for the clarification.
If not an asterisk, they’ll just have less impact. A proof generates a fact. The best facts and proofs are useful in that they help other things. You work becomes useful for my work, which may become useful for others.
It's still just as useful. The fact that's proven is what helps other proofs.
A computer assisted proof is just as correct or helpful, it just may be more complicated of a proof initially. Given time said proof can be simplified but having the proof in the first place allows you to move away from assumptions into proofs or alternatively even open new doors that weren't known to exist.
Keep in mind that these computer aided proofs are equivalent to pen and paper proofs but because you can rely on software to guarantee you haven't made any mistakes, you can make more complex proofs that still work.
It's the same as with programming. You can write overly complex and opaque proofs in the same way you can write bad, slow, or hard to read code. It still "works" but it's not ideal and is often a first revision in a series of steps towards the clean, fast, and easy to read final products.
The best proofs are good explanations as well as just being correct. If you don’t understand the theorem and the proof as well, you’re less likely to use it.
Presumably the asterix denotes "actually true"? ;-)
I don’t understand the chess analogy. How is it in any way similar?
Lean and the other theorem provers turn mathematical proofs into levels of a computer puzzle game, much like a chess puzzle.
Last time someone talked about automating proofs, a whole new field was invented (computer science)
They did the same with Prolog in 70" and... failed. Nothing new.