Hacker News Reader

Comment by rowanG077 | Hacker News Reader

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?

View on HN

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.

Disclaimer: I am a Lean/mathlib user.

> [citation needed]

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.

Such a hoogle analogue exists! See moogle.ai.

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.

Speaking of Hoogle, there's Loogle by Joachim Breitner: https://loogle.lean-lang.org/

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.

Reply on news.ycombinator.com