I helped a very little with the formalization (I filled in some trivial algebraic manipulations, and I was there for some Lean technical support).
It's exciting to see how quickly the work was done, but it's worth keeping in mind that a top mathematician leading a formalization effort is very exciting, so he could very easily scramble a team of around 20 experienced Lean users.
There aren't enough experienced Lean users to go around yet for any old project, so Gowers's point about ease of use is an important one.
Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib. It's reassuring that mathlib is being developed in such a way that new mathematics can be formalized using it. Like usual though, there was plenty missing. I think this drove a few thousand more lines of general probability theory development.
> Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib
Yes but the bulk of the work on this project was background as well. So the ease of use problem should be solving itself over time as more and more prereqs get filled in.
BTW, I find it interesting that mathlib is apparently also getting refactored to accommodate constructive proofs better, as part of the porting effort to Lean 4. This might encourage more CS- and program-verification minded folks to join the effort, and maybe some folks in math-foundations too (though Lean suffers there by not being able to work with the homotopy-types axioms).
Yes, sure, and that's how mathlib usually gets developed, project by project and PRing missing background material. I'm one of the mathlib maintainers, and I wanted to be sure there's acknowledgment here for the years of Boubaki-style work among hundreds of volunteers to build up the mathematics. In a way, now that the paper's been formalized it's time for the really hard work, which is figuring out how to restructure it (and mathlib) so that it can easily support future work. That's writing libraries for you.
Where are you getting the idea mathlib is being refactored for constructive proofs? I wouldn't say that's on the road map. In fact, the core Lean developers are uninterested in pursuing supporting this.
Since you're here, are you able to say why constructive proofs are interesting to program verification or (T)CS people? I've never heard anyone in TCS even know what constructivity is -- Lean supports their case where you write a program/algorithm and then (with classical logic) prove correctness and other properties. What would constructive logic give them?
I'll mention that the "Lean way" for constructivity is that you write `def`s for constructions. These can depend on classical reasoning for well-typedness if you want (like for being sure a number is in range when indexing an array), but there is a computability checker. In particular, the compiler sees if there is a way to lower the `def` into some simply typed IR, and this IR can be further compiled to C. If you trust the compiler, then you can trust whether it's real construction.
(Of course, you can also go and prove a definition evaluates to some value if you don't want to trust the evaluator.)
> [W]rite a program/algorithm and then (with classical logic) prove correctness. What would constructive logic give them?
Compared to the usual case of writing the "algorithm" (i.e. the construction/decision part) and "proof" separately, it basically offers better structuring and composability. Imagine writing an "algorithm" that itself relies for correctness on non-trivial preconditions, or must maintain some invariants etc. Proving correctness of a complete development that might involve wiring up several of these together is quite possible if you can use constructive proofs, but becomes quite tedious if you have to work with the two facets separately.
> Where are you getting the idea mathlib is being refactored for constructive proofs?
It's not being refactored for constructive proofs, but proofs that do use classical reasoning are being marked as such in a more fine-grained fashion rather than leaving it as the default for the entire development. Which makes it at least possible to add more constructive content.
Yeah, I can imagine that, and I've used sigma types to carry it out (`Subtype`s in particular, or perhaps custom structures). Why does the proof in the sigma type have to be constructive?
Certainly this is the road to "dependently typed hell" and it's good to avoid mingling proofs with data if you can, but avoiding the law of the excluded middle doesn't make any of that any easier.
This is also a bit of a distraction since what I really mean regarding TCS is that in my experience is that they do not see the proofs themselves as being objects-with-properties. They're perfectly happy with non-constructive reasoning to support constructions. I am looking to be convinced that constructive logic is worth it, but this mathematician hasn't seen anything compelling beyond work on foundations themselves.
Regarding mathlib, could you say what in particular you're talking about, since it's not ringing a bell, and I follow the changelogs.
> Regarding mathlib, could you say what in particular you're talking about, since it's not ringing a bell, and I follow the changelogs.
There's been several commits where general appeals to classical reasoning in some development have been replaced by more fine-grained assumptions of decidability for some objects, or marking uses of classical reasoning in some specific proofs. This has not happened throughout mathlib of course, just in some specific places. But it might still show one way of making the development a bit friendlier to alternate foundations.
> ...but avoiding the law of the excluded middle doesn't make any of that any easier.
Constructivist developments are not about "avoiding the law of excluded middle". They're more about leveraging the way we already structure mathematical proofs (and mathematical reasoning more generally) to make it easier to understand where simple direct reasoning has in fact been used, and a theorem can thus be said to be useful for such purposes. If all we did was proofs by contradiction and excluded middle, there would be no point to it - but direct proof is actually rather common.
> Why does the proof in the sigma type have to be constructive?
It doesn't, if the constructibility part has been stated separately (e.g. stating that some property is decidable, or that some object is constructible). That's in fact how one can "write the program/algorithm and the logic separately" in a principled way.
> I am looking to be convinced that constructive logic is worth it, but this mathematician hasn't seen anything compelling beyond work on foundations themselves.
This paper https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016... provides a reasonable summary of the relevant arguments. It's notable that a number of mathematicians are doing work that involves, e.g. the internal language of topoi, which pretty much amounts to invoking constructive foundations despite starting from what's otherwise a "classical" setting. That they go to all this trouble to do this certainly suggests that they find that work compelling enough. And indeed, it has practical implications wrt. e.g. alternate foundations for analysis, differential geometry etc.
Many times, Decidable assumptions are added simply because they appear in the terms in a theorem statement, and doing so makes applying such a theorem easier. There's the technical annoyance that Decidable instances are equal but not necessarily defeq, so if the wrong instances are present (such as the classical ones) then you need simp-like automation to rewrite instances before unifying. Maybe this is what you're seeing?
There have also been attempts to make polynomials computable, which peppers everything with decidability, but it's not a good data type for real large-scale computations, so it's not clear what the future is there. Maybe the defeqs are worth it, I don't know.
Re constructibility, this is all at too high of a level to really know what you're talking about, or why it's beneficial to write proofs themselves in a certain way. I'm not really even sure what you mean by "constructive". To me, I see no problem with writing a recursive definition that requires a non-constructive proof of termination by well-founded recursion -- is that constructive to you?
AIUI, the fact that well-founded recursion is encoded as "noncomputable" in Lean is just a wart/quirk of that particular system; it can be justified in dependent type theory which is quite constructive and used by other systems such as Coq.
It's not `noncomputable` in Lean though. Lots of computable functions use it.
I've read Bauer's paper before btw. I think topoi are cool, but I don't think it's a complexity worth thinking about for everyone else who isn't concerned about these things.
Since I have been part of many such grinds that are now big data sets, I can honestly tell you that it is one of the best things in the world. I know that those thousands of hours of my work has led to 100x savings for other people. I also met people and could work on problems I would never get in professional life.
Since you seem to be an expert on this matter I have always wondered whether at some point it becomes faster to prove novel theorems using a theorem prover then doing it on paper. I imagine that quite a bit of time is wasted in proving things that are already proven. In a similar manner that if there would be no libraries, just snippets of code in papers, in computer programming a lot of time would be wasted writing the same things again. I imagine a "proof finding" tool like hoogle is a "function finding" tool could provide a lot of value here. What is your perspective on this?
The biggest benefit of a formalized theorem library is not so much proving entirely new theorems (though it helps a little bit I suppose) but refactoring the existing developments to make them more elegant, easier to understand, and enhance their generality. In fact, it's already the case that the average formal proof is written to be somewhat higher in abstraction and more straightforward in reasoning than the informal counterpart.
This kind of refactoring work is quite hard to do with paper proofs alone, since one cannot essily be sure whether they've preserved correctness wrt. the original development. Having a proof assistant really is a big help there.
> The biggest benefit of a formalized theorem library is not [...] but [...]
[citation needed]
I think there are many benefits. Hard to claim that your favourite one is the biggest benefit.
In general, I think it's a bit weird that you are repeatedly (also other HN threads, and sibling comments in this one) making unfounded claims about Lean/mathlib, to the point where you are telling maintainers how their system works. And if they explain that you are misunderstanding the system, you ignore their correction and bring up the next (or the same) unfounded claim.
Whoops, you're right. Here's what Fields medalist Terence Tao has to say about it: https://terrytao.wordpress.com/2023/12/05/a-slightly-longer-... "...sometimes, after a proposition has been proven, someone in the project realizes that in order to apply the proposition neatly in some other part of the project, one has to slightly modify a hypothesis ... Often one can just modify that hypothesis and watch what the compiler does. ... [W]ith well-designed proofs, the process of modifying a proposition is often substantially easier than writing a proof from scratch. (Indeed it is this aspect of formalization where I think we really have a chance in the future of being in a situation where the task is faster to perform in a formal framework than in traditional pen-and-paper (and LaTeX) framework.)"
> And if they explain that you are misunderstanding the system
I don't think that's a fair description of the sibling threads. If a mathlib maintainer says "no, we're not going to avoid LEM/by-contradiction everywhere in our proof library, that would be silly" because that's what most mathematicians today think constructivism means, as in rejecting the bulk of existing math entirely as meaningless - and then they add "but yes, there are places where we want to work with our own assertions about decidability, and not let classical reasoning mess that up" I think it's entirely fair to call the latter pretty close to a constructivism-friendly approach.
(Keep in mind that most practicing mathematicians don't work with foundations, so the fact that misconceptions like the above would be widespread is not surprising. The remaining argument is about the increased complexity of constructive reasoning, and it's entirely fair for a practical development to want to avoid that, and just work with classical statements. After all, most of the mathematical literature is indeed classical; it does not bother with the computational aspect or with the perceived messiness of numerical analysis.)
> we want to work with our own assertions about decidability, and not let classical reasoning mess that up
I am not confident that you understood what I meant. It has nothing to do with the proofs themselves, but a mathematically uninteresting matter about whether or not you can rw/simp using the theorem due to the statement incidentally containing concrete Decidable instances (it's simply a weakness of these tactics that they are not able to make use of the fact that types are Subsingletons, so if Decidable instances aren't free variables the theorems might not be applicable). There are some old parts of the library that come from probably Lean 2, like Finset, that are fairly constructive, and, since the most developed finite sets are these Finsets, and many of their operations require Decidable instances in their definitions, many theorems about finite sets mention Decidable instances. It's a matter of how much engineering time is available among all the volunteer contributors (along with some fond feelings for Finset since it's been around so long) that we haven't switched over to using the subtype of Set satisfying Set.Finite, which is very non-constructive but would make our lives easier.
I'll emphasize that this rw/simp issue is not about classical reasoning. Even if you banish classical reasoning from the library, it plagues Decidable instances everywhere, and special attention must be made to ensure that theorem statements contain no concrete Decidable instances. Getting this right is an annoying distraction that does not enable any new features or insight.
I'll also emphasize that mathlib theorems do not have Decidable instance hypotheses that are only used in their proofs. Last I checked, there's even a linter for this.
> I don't think that's a fair description of the sibling threads.
Since we're talking about others' "misconceptions", am I right that you weren't aware that in Lean you can do well-founded recursion using a classical termination proof and get a computable function? That's the sort of thing I was trying to make sure we were on the same page about. I brought up LEM to feel out your position because that's what plenty of people mean by constructivism, and I honestly have not been able figure out what constructivism means to you and what sorts of concrete benefits you think constructivist proofs give you. If you're able to interleave a construction with classical reasoning arguing that the construction is well founded, then what is it that the CS and program verification folks are missing from Lean? That's what I'm missing here. (And if there's a good concrete answer the folks who develop Lean itself would be interested.)
To be clear, there are plenty of things missing from Lean that would definitely help CS and program verification folks, but as far as I know none of these features touch upon constructivism.
While I wouldn't say that there are no benefits to constructive reasoning, and I support the work people do on foundations, all these Decidable instances really add to the difficulty that people experience learning to do mathematics in Lean.
I'm sure there are people out there doing program verification that think about it using topos theory, but I suspect it is very few. That's hardly a justification to put resources into making proofs be constructive mathlib-wide.
The basic definition of wellfoundedness in Lean and mathlib is in fact constructive, same as in Coq. There are technical implications to being able to reason 'classically' about well-founded relations but they apparently are fairly minor, having to do with the "no infinite chain" definition of well-foundedness. https://proofassistants.stackexchange.com/questions/1077/wel... -- and actually, this requires a form of choice in addition to classical reasoning. Mathlib knows about this, it's in https://leanprover-community.github.io/mathlib_docs/order/or... .
I think I've emphasized above that constructivism is more about preserving and leveraging the implied computational content of existing proofs than insisting on constructive proofs everywhere - the latter in particular adds a lot of complexity even when it's actually feasible, so I agree that Mathlib shouldn't do that. But when something can be phrased as a computable construction or decision procedure "for free" simply by relying on straightforward direct reasoning and eschewing classical assumptions, it makes sense to enable that, including as part of a mathematical library.
I'm by no means an expert on interactive theorem proving -- I'm just a Lean user who knows a lot about how Lean works, and I got into it while procrastinating finishing my math PhD.
I think writing novel theorems directly in Lean is similar to the idea of architecting a large software system by jumping right into writing code. Certainly for small things you can just code it, but past a certain level of complexity you need a plan. Paper is still a useful tool in programming, and theorem proving is just a kind of programming.
During my PhD I occasionally used Lean to check whether some ideas I had made sense. They were more of a technical flavor of idea than what I'd usually think of a novel theorem being, and where Lean was helpful was in keeping track of all these technical details that I didn't trust myself to get completely right.
Speaking of roadmaps, one tool large formalization efforts use are blueprints, an idea developed by Patrick Massot. Here's the one for Tao's project: https://teorth.github.io/pfr/blueprint/dep_graph_document.ht... On this webpage there are also LaTeX versions of every main theorem and links to their Lean equivalents. The original paper was not formal enough to directly formalize in a theorem prover, and this blueprint represents the non-trivial additional creative effort that went into just planning out how to code it.
There's also an AI-driven free-form text tool that recently appeared: https://www.moogle.ai/
A funny thing about libraries saving people from wasting effort redoing things is that, while on one hand this is true that having centralized repositories of knowledge invites people to contribute to them and reuse their work, on the other what can happen is that philosophical differences can cause schisms and result in n-fold duplicated work. (Consider the endless web frameworks out there!) Even Lean could be such a duplication since there's already Coq, Agda, HOL, etc. So far, Lean's mathlib has managed to remain a single project, which I think is an important experiment in seeing if all of mathematics can be unified in a common language. Mathlib is a strange compared to normal software libraries, since its goal is to eventually consume every downstream project that's ever created. If this model can continue to scale, then that makes the question of whether something's been formalized yet or not simpler. Though, even now, there's so much code in mathlib that sometimes you need to go to leanprover.zulipchat.com and ask, and someone familiar with the right corner of the library will usually answer reasonably quickly.
One silver lining for n-fold duplication is that it's usually not a complete reinvention, and this gives variants of ideas an opportunity to explored that otherwise would succumb to the status quo. I feel that even when someone re-formalizes a theorem, it's an additional opportunity to evaluate how this knowledge fits into the larger theory.
> on the other what can happen is that philosophical differences can cause schisms and result in n-fold duplicated work
It would indeed be nice to have a principled answer to the issue of differing foundations, including e.g. working in ZF(C) vs. type theory. (The dirty little secret there - and what makes mathlib more popular than it might be otherwise - is that while most practicing mathematicians appeal to ZF(C) as their default foundation they don't actually work with it in a formal sense, and the way they do reason about math is a lot easier to account for in type theory. See also https://math.andrej.com/2023/02/13/formalizing-invisible-mat... ) I guess the closest thing we have to that is logical frameworks, which are designed to accommodate even very weak/general foundations at the outset and "bridge" theorem statements and proofs across when needed.
( https://westurner.github.io/hnlog/#story-38435908 Ctrl-F "TheoremQA" (to find the citation and its references in my local personal knowledgebase HTML document with my comments archived in it), manually )
> TIL i^4x == e^2iπx ... But SymPy says it isn't so (as the equality relation automated test assertion fails); and GeoGebra plots it as a unit circle and a line, but SymPy doesn't have a plot_complex() function to compare just one tool's output with another.
That's a lot of links to take in, and I don't do really anything with ML, but feel free to head over to https://leanprover.zulipchat.com/ and start a discussion in the Machine Learning for Theorem Proving stream!
My observation at the moment is that we haven't seen ML formalize a cutting-edge math paper and that it did in fact take a lot of experience to pull it off so quickly, experience that's not yet encoded in ML models. Maybe one day.
Something that I didn't mention is that Terry Tao is perhaps the most intelligent, articulate, and conscientious person I have ever interacted with. I found it very impressive how quickly he absorbed the Lean language, what goes into formalization, and how to direct a formalization project. He could have done this whole thing on his own I am sure. No amount of modern ML can replace him at the helm. However, he is such an excellent communicator that he could have probably gotten well-above-average results from an LLM. My understanding is that he used tools like ChatGPT to learn Lean and formalization, and my experience is that what you get from these tools is proportional to the quality of what you put into them.
Communication skills, Leadership skills, Research skills and newer tools for formal methods and theorem proving.
The example prompts in the "Teaching with AI" OpenAI blog post are paragraphs of solution specification; far longer than the search queries that an average bear would take the time to specify.
Is there yet an approachable "Intro to Arithmetic and beyond with Lean"? What additional resources for learning Lean and Mathlib were discovered or generated but haven't been added to the docs?
Perhaps to understand LLMs and application, e.g. the Cuttlefish algorithm fills in an erased part of an image; like autocomplete; so, can autocomplete and guess and check (and mutate and crossover; EA methods and selection, too) test [math] symbolic expression trees against existing labeled observations that satisfy inclusion criteria, all day and night in search of a unified model with greater fitness?
It's exciting to see how quickly the work was done, but it's worth keeping in mind that a top mathematician leading a formalization effort is very exciting, so he could very easily scramble a team of around 20 experienced Lean users.
There aren't enough experienced Lean users to go around yet for any old project, so Gowers's point about ease of use is an important one.
Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib. It's reassuring that mathlib is being developed in such a way that new mathematics can be formalized using it. Like usual though, there was plenty missing. I think this drove a few thousand more lines of general probability theory development.