Lean vs other systems

Stream: general

[Juho Kupiainen]

There are many systems that allow you to write and check proofs written in a formal language. Lean, Metamath, Isabelle HOL, Coq, ACL2, Agda, Albatross, F*, HOL Light, HOL4, LEGO, Mizar, NuPRL, PVS, Twelf

I'm just wondering if we are better or worse off having all these different systems. Should we all just stick to one and build a good library in it, or is there some fundamental reasons why one is better than another. Yes, Lean has a computational component that Metamath doesn't, but nothing is stopping you from writing a model of a real computer in Metamath. Yes, Lean has proof automation that Metamath doesn't have, but aren't big general theorems exactly the same as proof automation? I'd personally be especially interested in hearing @Mario Carneiro s thoughts on this. Pondering this I'm reminded of a song called "One Vision" by Queen..

[Mario Carneiro]

I am largely agnostic as to foundations. But I do think that we should make every effort to connect all the proof systems together, because how else can we make proofs "stick"? It would be quite the nightmare if we can never get off the ground because we reinvent natural number addition every five years in a new system

[Mario Carneiro]

Actually, I prefer simple foundations to complex ones because the complex foundations fool you into thinking that you have something that is easier than it is; as soon as you stray from what the axioms give you things become hard again

[Juho Kupiainen]

Are things easier in Lean though, than in Metamath, after having actually tried to do complicated things in Metamath?

[Mario Carneiro]

The most important feature a foundation has is expressivity, the ability to define the things people care about, with proportional overhead (not exponential overhead!). If you can't write X in the system, then you are doomed, although you can delay the inevitable for a while

[Mario Carneiro]

The problem with questions like that is it presupposes that Metamath and Lean are trying to solve the same problems, and they aren't

[Mario Carneiro]

Metamath is a logical foundation and a verification system. It has a "build your own" user experience

[Mario Carneiro]

so asking if Metamath has tactics is beside the point; it's not supposed to have tactics, it's a foundational system

[Mario Carneiro]

Of course you want tactics and a nice user experience, but I think metamath is one of the few systems that conciously separates this from the verification aspect

[Juho Kupiainen]

I'm just wondering whether there is any fundamental reason why writing general theorems in metamath in order to help proving things is any different from writing tactics in Lean?

[Mario Carneiro]

Theorems and tactics are different. A tactic is more like a metatheorem, a family of related theorems that are all provable

[Kevin Kappelmann]

btw. there are efforts to connect theorem provers, e.g. Logipedia/Dedukti

[Mario Carneiro]

the downside of a tactic is that you have to run it every time you want a new proof, whereas you can check a theorem once and use it as many times as you like

[Juho Kupiainen]

I'm not an expert on this so please correct me if I'm completely wrong, but doesn't expressive foundations allow you to write category theory kinds of general theorems that are basically the same thing as tactics? I'm just guessing.

[Mario Carneiro]

An example of something that can't be proven by a single theorem is norm_num

[Mario Carneiro]

that is, evaluating arbitrary arithmetic expressions

[Juho Kupiainen]

So the problem is that you can't make the metamath proof checker do complex calculations? You have to spell out the calculations in the proof? and then you need to have a metasystem that writes those long calculations?

[Mario Carneiro]

yes

[Juho Kupiainen]

But is this actually true?

[Mario Carneiro]

This is a benefit

[Mario Carneiro]

By an appropriate sequence of lemmas, you can make the metamath proof checker perform any computation in NP

[Mario Carneiro]

the same holds true for lean btw

[Juho Kupiainen]

So there is no way to make metamath proof checker perform an arbitrary calculation by writing down the definition of the calculation as a turing machine and proving that the calculation terminates? Because if you could, couldn't you somehow transfer the calculation work on to the proof checker side? that is make a tactic that's written inside the system?

[Juho Kupiainen]

As in you can't say, this theorem holds because this tactic proof searching algorithm is proven to terminate, and the proof is simply to run the program?

[Mario Carneiro]

You have to provide a proof that the TM evaluates to some particular value, and that means roughly one proof step per TM step

[Mario Carneiro]

so the longer the program runs, the longer the proof gets

[Mario Carneiro]

metamath doesn't support extending the kernel by a verified computation. I hope to add this capability to MM0 after the bootstrap

[Mario Carneiro]

It's still pretty darn fast without it

[Juho Kupiainen]

So, the point is that tactics may not terminate, and you can't make a proof checker run something that may not terminate. and metamath is only a proof checker.

[Mario Carneiro]

this theorem holds because this tactic proof searching algorithm is proven to terminate

It would be a very strange theorem that would not be provable outright if you had this property

[Mario Carneiro]

the only reason it doesn't work for things like norm_num is because the theorems are not uniformly describable

[Mario Carneiro]

termination or lack thereof is not a problem. Metamath simply doesn't know how computers work so it can't extend itself with a computer program given by the user

[Mario Carneiro]

If we're running the program, then there is no problem with termination - we continue verification only after it returns, so if it never returns then we never finish the proof

[Mario Carneiro]

If we are not running the program, and are simply using the existence of the program to prove the theorem, then we may as well chuck the program and prove the theorem directly

[Juho Kupiainen]

I'm just guessing again but isn't the point of all these new type theory systems to kind of make a unification algorithm that can be easily used as a general purpose computer?

[Mario Carneiro]

that's the theory...

[Mario Carneiro]

turns out computers are better at being computers than unification algorithms are at being computers

[Kenny Lau]

theory and practice are the same in theory but not in practice

[Juho Kupiainen]

I like how metamath is such a simple system and then you just have a list of axioms. Could we do kind of a similar thing where we could extend the unification algorithm by just adding an extra axiom?

[Mario Carneiro]

Lean is actually extensible in this way, but it's a "big boy" feature and was not entrusted to us. Currently the only extensions to the normalization algorithm are quotients and inductive types

[Mario Carneiro]

If you add your own rules it becomes very easy to loop or lose some metatheoretic property

[Mario Carneiro]

and you will almost certainly make defeq undecidable

[Mario Carneiro]

Basically, in DTT defeq is "second class" equality - it's never strong enough, but you can't just ignore it. I like that in metamath there is only one equality

[Juho Kupiainen]

But couldn't you just add a feature that allows you to prove things by saying that the proof exist because a computation terminates, and then you can just add a "proof by termination" and the checker runs the computation. Of course you may not actually have the proof.

[Juho Kupiainen]

But thats basically what a tactic is.

[Mario Carneiro]

right, that's what I mean by extending the kernel with a verified computation

[Mario Carneiro]

that's not the same as a tactic, which is a proof-producing program

[Mario Carneiro]

metamath prefers to deal with tactics in that sense, because the checker doesn't have to know anything about the tactic for the system to work

[Juho Kupiainen]

Well, basically the same, as the program may not actually terminate when you write "proof by termination" and run the checker?

[Mario Carneiro]

The checker is given the output of the tactic as its input. It is never given the opportunity to run the tactic itself

[Mario Carneiro]

so when you start the checker you already have the proof of termination in hand

[Juho Kupiainen]

Ah, right. A tactic would be adding that the program terminates as an axiom.

[Juho Kupiainen]

And seeing what happens.

[Mario Carneiro]

Lean doesn't have trusted computations either btw

[Mario Carneiro]

It very nearly does, but you can't use #eval to prove a reflexivity

[Juho Kupiainen]

I want to build my own proof system. Maybe we should collaborate on extending metamath? Personally, I'd like to build a system where you can solve real world problems by checking proofs in order of length.

[Mario Carneiro]

that will never scale unfortunately

[Mario Carneiro]

the number of proofs grows exponentially

[Juho Kupiainen]

Well, it of course depends on the language. There's always some weird language where it works, of course. Because you can always put the computation on the checker side.

[Mario Carneiro]

There actually was a competition of sorts to find the shortest proofs of a bunch of basic propositional logic problems, and many of them were found by exhaustive search, but you hit a wall at about 18 steps

[Juho Kupiainen]

I think a big problem in computer systems is fragility, that is, systems work great, until they don't.

[Juho Kupiainen]

Like, some tactic might work great, until it doesn't. And then the next best thing is basically to go through proofs in order of length.

[Mario Carneiro]

Whenever you are solving an exponential problem it always looks like that. You might push the wall back a few steps with a different formalism, but you can't eliminate it unless your language is trivial

[Juho Kupiainen]

Having reasonable solutions there in between is where the improvements in systems happen.

[Mario Carneiro]

machine learning is all about trying to solve these problems by finding structure in the search (something better than "shorter is better")

[Juho Kupiainen]

I mean reasonable solutions for practical problems, you obviously can't have reasonable solutions for all problems.

[Juho Kupiainen]

I think trying to build something between the two ends of search proofs by length and a few tactics that solve simple problems would be to work on trying to "dig a tunnel" from both ends, trying to make searching proofs in order of length better while making tactics better.

[Mario Carneiro]

that at most doubles the distance to the wall

[Juho Kupiainen]

I mean I just think it could provide ideas to look at things from many angles.

[Kevin Buzzard]

I'm just wondering if we are better or worse off having all these different systems. Should we all just stick to one and build a good library in it

Of course the problem with this is that everyone thinks that everybody else should be using their system. It also all depends on what your goals are.

The work of Rob Lewis and his collaborators, and the perfectoid project, are attempts to prove that Lean is capable of doing modern mathematics which "proper mathematicians" are interested in (this is a tongue-in-cheek phrase referring to people doing stuff like number theory/algebra/analysis/geometry etc in maths departments, as opposed to all the category theory / type theory people working on foundations). Sebastian Gouezel has produced work in Isabelle/HOL which is also mainstream mathematics done in a theorem prover. But we are in the minority here -- most work done in these systems is not an attempt to do modern mathematics on a computer. For example my impression is that Agda is a fascinating experiment to see what kinds of fancy inductive-recursive-inductive types one can get away with whilst preserving soundness. That's great, but guess what? The perfectoid project does not contain one single instance of the inductive command. Us "proper mathematicians" just need structures.

or is there some fundamental reasons why one is better than another.

People can certainly argue about this point all day. I think that dependent type theory is currently our best option for "all of pure mathematics" and I think that Lean is currently our best option for dependent type theory, but plenty of people have plenty of other opinions. The reason I like my opinion best is that I am one of few "proper mathematicians" who is even in a position to have an opinion, and when I hear other people talking about what they think mathematics is and how it fits best into their systems, I often find that the underlying disagreement is actually the question of what mathematics is. I am attempting to represent the generic pure mathematician who works in a generic mathematics department.

As is the case for programming languages in general, the best tool for the job depends very heavily on what the job is. An analogue of your question might be "I'm just wondering if we are better of worse off having all these different programming languages -- C, Rust, Java, Python, x86 assembly. Should we all just stick to one?"

[Juho Kupiainen]

To me, as someone who isn't that knowledgeable of foundational systems, it seems like a pretty practical way to describe a foundational system would be a list of axtioms that state that a computer program terminates. The lengths of various proofs and relative (between theorems) performance of the checker would be determined by which axioms you add. You could make a checker that both runs a computation to check for the proof and at the same time searches for proofs that the computation terminates so as to not have to do the computation. And I guess you can also describe the axiomatic content this way as well.

[Chris Hughes]

To me, as someone who isn't that knowledgeable of foundational systems, it seems like a pretty practical way to describe a foundational system would be a list of axtioms that state that a computer program terminates. The lengths of various proofs and relative (between theorems) performance of the checker would be determined by which axioms you add. And of course you can describe the axiomatic content this way as well.

I guess this list of axioms are more or less the rules for recursors of inductive types.

[Olli]

I have a related question about foundations and how they play with different proof systems.

I've been reading about topos theory lately, which I understand in some ways is an alternative foundations for mathematics, where there's a clearer distinction between the types of foundational assumptions we make.

This may sound hilarious to the mathematicians, but as a programmer I think of it as being a foundation with built-in axiomatic/foundational polymorphism, in the sense that I can define mathematical objects like the real numbers that are independent of the topos I work in, so by delaying the choice of topos that restricts the type of things I can say, I get a nicer organization of theorems based on the types of assumptions that have been made.

So to my naive understanding, it feels like doing math in topos theory is analogous to following good software engineering practices in maintaining a large code base. Is this a valid comparison?

If so, does the choice of foundations between something like Metamath/STT/DTT make a difference in working towards a goal like this?

[Mario Carneiro]

relative (between theorems) performance of the checker would be determined by which axioms you add.

If you need to add axioms to make a proof check faster (by more than a constant additive factor), then the prover is not expressive enough

[Mario Carneiro]

If so, does the choice of foundations between something like Metamath/STT/DTT make a difference in working towards a goal like this?

Note that Metamath does not belong on that list - it is not a mathematical foundation, it is an environment that lets you define your mathematical foundation. Isabelle has a similar distinction, if you are familiar with the difference between Isabelle/Pure vs Isabelle/HOL.

Most formal systems let you pick your axioms, although lean doesn't really let you turn off a great deal of axioms that you might not want (like universes or proof irrelevance). To me, your topos theory example is similar to proving theorems with attention paid to the axioms you use. In metamath this is easy because the axioms are quite fine grained - there are 30 or so of them, leading to 2^30 different subsystems of ZFC you could study; or just forget ZFC and add your own axioms if you prefer something else. Lean has only 3 axioms, and the only really useful one to avoid is choice, so reverse mathematics is a non-starter.

[Olli]

Could you define CoIC inside Metamath and then work using that?

[Mario Carneiro]

Yes

[Mario Carneiro]

I got most of the way to doing that with lean, but that was before my masters thesis so I wasn't really sure what the axioms for inductives were

[Mario Carneiro]

MLTT is not difficult

[Mario Carneiro]

There is a HOL library for metamath available at http://us.metamath.org/holuni/mmhol.html

[Mario Carneiro]

the real bottleneck is usually getting an exact statement of the axiomatic system

[Olli]

Ok, yeah I can see the analogy with it being the assembly language for proofs.

[Olli]

For my example with topos theory, let's say I make a definition that works in any elementary topos, and then I define a new topos, I can do this in independent order, and as soon as I'm done I should get a bunch of free theorems. If one was working in Metamath, then it feels like you'd have to be working one level higher, where the free theorems get automatically generated, does this sound correct?

[Mario Carneiro]

If you prove a theorem using axioms A, B and apply it in a context where you are also assuming C, you don't need to do anything special

[Mario Carneiro]

What you don't get with this kind of embedding is the ability to reinterpret symbols. For example, if I prove a fact like foo = foo where foo is a "fixed constant" about which I know nothing, I cannot apply it with foo := 2. I can add an axiom saying foo = 2, and then foo acts like a definition, but I can't also add a definition foo = 3 because that would be inconsistent

[Mario Carneiro]

In order to really do the topos theory approach justice, you have to deep embed it, getting something more like the category theory library

[Mario Carneiro]

this comes with some notational overhead unless you design the tool to deal with terms of this form

[Olli]

right, the reason we have higher level programming languages is not just to avoid typing less, but because our intended meaning of the program is better captured at a higher level, because the lower level aspects are deemed implementation details.

[Olli]

MM1 is higher level than MM0 is higher level than Metamath if I've understood things correctly

[Mario Carneiro]

MM0 is more complex than metamath but they are equally expressive. MM1 is sugar over MM0

[Olli]

ah right

[Mario Carneiro]

"higher level" is perhaps not the right characterization. All of them are capable of speaking at quite high levels mathematically

[Mario Carneiro]

the thing that is low level is the actual mechanics of proving theorems. It's not like with computer languages where the low level languages are concerned with completely different things, different levels of abstraction

[Olli]

Hmm yeah it is possible that I fail to notice my own bias with thinking about software/programming languages.

When I say higher level proof language, I mean a language that generates proofs that have a lot of repetition. The way Metamath allows you to inspect proofs down to very low level of detail is very nice, but the issue I have in mind is that if I write a definition in this higher level language, then the best way to understand its meaning is by reading it at this level, because we want to hide the repetition to increase the signal/noise ratio. Do you see this not being an issue?

[Olli]

I can give an example I have in mind: Take Lawvere's Fixpoint Theorem, that generalizes many other fixpoint theorems. I would like to see not just the proof of the LFT itself, but also how other theorems are instances of it. To me it feels like you would need to work on a higher semantic level than MM0 in order to do this, but maybe I'm mistaken?

[Mario Carneiro]

When I say higher level proof language, I mean a language that generates proofs that have a lot of repetition. The way Metamath allows you to inspect proofs down to very low level of detail is very nice, but the issue I have in mind is that if I write a definition in this higher level language, then the best way to understand its meaning is by reading it at this level, because we want to hide the repetition to increase the signal/noise ratio. Do you see this not being an issue?

Metamath is actually very non-repetitive, MM0 even more so. It would be nice to have some theorems about this, but they are pretty close to optimal. The repetition you see in the web page presentation is because each line is independent of the others, and common subterms are expanded during printing. In the actual proof it's totally deduplicated

[Mario Carneiro]

I can give an example I have in mind: Take Lawvere's Fixpoint Theorem, that generalizes many other fixpoint theorems. I would like to see not just the proof of the LFT itself, but also how other theorems are instances of it. To me it feels like you would need to work on a higher semantic level than MM0 in order to do this, but maybe I'm mistaken?

I don't know what Lawvere's Fixpoint Theorem is, but I'm 100% confident you can state it as a single theorem of MM/MM0. If you want to apply it in a particular circumstance, you prove that your category instantiates the assumptions, unfold the meaning of the symbols (i.e. maybe you want to replace "generic morphism" with "function") in the statement, and that's it.

[Mario Carneiro]

the considerations are roughly the same if you wanted to do the same thing in lean. Declare the general concept of a category, do your work there, then instantiate the theory in the concrete case

[Mario Carneiro]

Lean is actually far more repetitive than Metamath. This is the result of things like tactics that don't clean up after themselves in the output proof, congr generating congr lemmas from scratch every time it's called, typeclass inference not saving and reusing typeclass lookups, and kernel rfl proofs, which have to unfold huge equation compiler terms

[Mario Carneiro]

Metamath looks more repetitive because of its print settings, but exactly because of that people have a much greater incentive to minimize repetition. In other theorem provers all the junk is hidden under the rug

[Jesse Michael Han]

to clarify, Lean is far more repetitive than Metamath during compilation/tactic execution; this is the cost of automation which allows the user to work at a higher level when writing Lean source code

[Jesse Michael Han]

of course, your Lean server recompiles every time more than 200ms elapses between keystrokes, and while ideally you don't notice this because of caching, it's not hard for users to get to a place where they experience significant lag waiting on elaboration, typeclass resolution, and tactic execution

[Jesse Michael Han]

@Olli note that Lean's implementation of DTT naturally has semantics in locally cartesian closed categories, so it's easy to shallowly replay the proof of the LFPT in Type:

import tactic

-- https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem

def δ {X : Type} : X → X × X := λ x, ⟨x,x⟩

def eval {A B : Type*} : (A → B) × A → B := λ pr, pr.1 pr.2

lemma lfpt {A : Type} {B : Type} (ϕ : A → A → B) (Hf : function.surjective ϕ) :
  ∀ f : B → B, ∃ s : B, f s = s :=
begin
  intro f, cases Hf (f ∘ eval ∘ (prod.map ϕ id) ∘ δ) with p Hp, use ϕ p p,
  conv_rhs { rw Hp }, refl
end

lemma cantor {X : Type} (ϕ : X → (set X)) : ¬ function.surjective ϕ :=
begin
  intro H, cases lfpt ϕ H (λ p, ¬ p) with p Hp, ifinish
end

[Olli]

@Jesse Michael Han thanks, I was going to attempt this on my own but it's good to have something to look at if I get stuck :)

[Olli]

@Mario Carneiro if I were to prove LFPT in Metamath and then show that Cantor's Theorem follows from it, would I be assuming lfpt and deriving canth, or would I have to make a new statement different from canth that I know means the same thing?

[Olli]

I think the larger issue I am trying to understand is if there is a way for me to see what are some examples of theorems/definitions that have very high generality (such as LFPT) simply by looking at the shape of the set of proof derivations in the database of theorems I'm working in (so probably set.mm in Metamath)

[Mario Carneiro]

You would apply lfpt to get something that is not exactly canth but is equivalent to it (defeq in lean terminology)

[Mario Carneiro]

you would have to postprocess the statement to get rid of the category theory notations

[Mario Carneiro]

There isn't that much category theory, but here's the yoneda lemma: http://us.metamath.org/mpeuni/yoneda.html

[Olli]

To continue with the analogy of maintaining software at large, I am wondering if we have the same conflict between adding new features (theorems) vs. abstracting/decoupling them from each other, and how much does the foundation we choose have to do with the ease of organizing things nicely

[Mario Carneiro]

I think that the cost of abstraction is higher in (formal) math than it is in software, because you have to filter everything through an extra definitional layer

[Mario Carneiro]

the foundation doesn't matter at all. The only thing a foundation can do for you is make certain things impossible and other things difficult

[Mario Carneiro]

the job of making things easy is left to the user interface

[Olli]

it's interesting to think about especially when it comes to the prospects of having some kind of an AI helping us do mathematics. The first thing that comes to mind is a superhuman tactic to solve a goal, but wouldn't it be even more valuable having suggestions on how to organize the material we already have in a way that makes expanding it easier?

[Mario Carneiro]

yes? What does that have to do with foundations?

[Mario Carneiro]

To give a simple example of why foundations don't matter, suppose I rewrote the lean kernel to produce typechecking proofs that it fed to metamath / ZFC as an oracle, and reports success if the backend prover accepts the proof. The front end wouldn't change at all, mathlib would still compile, you wouldn't even notice the difference - yet now the foundation is fundamentally different

[Mario Carneiro]

this is why I see a type system as a front end feature

[Olli]

if we think of the set of theorems we have as a data structure, then I think a highly general theorem such as LFPT should be a densely connected node, or there should be some metric for valuing these types of theorems over ones that are less general. I mean I am not a mathematician so this might be very naive, but if we were to throw process cycles at a database of theorems in the hopes of making breakthroughs that connect areas of mathematics we had not realized were related, then this type of activity would be essential

[Olli]

densely connected node is probably an incorrect description, but I hope you understand what I mean by valuing generality

[Mario Carneiro]

Honestly, given Jesse's demonstration of the proof, I don't value it very highly. The proof is apparently only two lines, which means that if you try to apply this theorem in a particular category the unpacking overhead will be more than the proof itself

[Mario Carneiro]

I always tend to get this impression from category theory proofs

[Mario Carneiro]

the savings from extracting a theorem is (number of uses - 1) * (size of proof) - definitions needed to state the theorem - (number of uses) * (unpacking overhead)

[Mario Carneiro]

if unpacking overhead is small and no new definitions are needed, then it's a pretty low bar to meet, but definitions and unpacking overhead often go together, and category theory is full of small abstract theorems

[Olli]

the unpacking overhead is high because it is applicable in a wider set of contexts, right? i.e. we are talking about breadth vs. depth

[Mario Carneiro]

Unpacking overhead depends on a few things. Roughly, it depends on the difference between the putative generalization and the concrete instance that it's supposed to be generalizing. Oftentimes it's a literal generalization, as in you have just universally quantified some variable that was already there. Rather than prove 2 + 3 = 3 + 2 we prove a + b = b + a. This kind of generalization has almost no overhead.

A bigger overhead comes from unpacking structures; for example we want that to follow from an abelian group axiom, so we have some <G, +> \in AbGroup and have a theorem <G, +> \in AbGroup -> a \in G -> b \in G -> a + b = b + a. This is still not so bad, because I've unfolded the structure. If it shows up bundled, it might instead be S \in AbGroup -> a \in carrier G -> b \in carrier G -> add G a b = add G b a and now we have to instantiate this with <G, +>, and then replace add <G, +> with + and carrier <G, +> with G everywhere they appear

[Mario Carneiro]

If, as in lean, we didn't bother to remember that e.g. int is an abelian group, but instead have to traverse the algebraic hierarchy to find the proof, then the overhead is a bit more.

[Olli]

right, so you are saying that you don't value this theorem as much because its abstractness makes it less useful in digging deeper faster, meaning it would not be a useful piece of a superhuman tactic, as it would slow it down.

What I am getting at is that this type of theorem is useful not as a building block, but as a goal in itself, i.e. I care less about theorems that go very deep, and more about the ones that bridge a lot of gaps.

[Olli]

I concede that what I initially wrote is what your point refutes, but it made me realize that an actually useful AI for doing mathematics probably should wrestle with these two conflicting goals of digging deep into a search tree, and the conflicting objective of organizing theorems in such a way that makes them slow to use (but insightful to read)