Theorem Proving in Lean [pdf] | Hacker News Reader

Theorem Proving in Lean [pdf]

leanprover.github.io

91 pointsfurcyd22 comments

I'll have to work through this when I get the time.

I started teaching myself Haskell for fun about a year and a half ago, and ended up going down a rabbit hole of formal logic, set theory, mathematical foundations etc. which I did not expect at all; I'm currently spending some time looking at algebraic topology to give me a grounding to go into homotopy type theory.

For anyone else with an interests in this area, I'd strong urge you to look at some of the work from Kevin Buzzard (Imperial College), perhaps better known as an algebraic number theorist, who leads the Xena [1] Project, which started as an attempt to completely formalise all the problem sheets for one of the undergraduate maths modules at Imperial in Lean. There's also a GitHub repo [2] with a lot of work to build on.

Adam Chlipala (MIT) also teaches a course in formal program verification in Coq based on his book [3] which is a valuable resource.

1: https://xenaproject.wordpress.com/

2: https://github.com/kbuzzard/xena

3: http://adam.chlipala.net/frap/

So is homotopic type theory just another way to look at the same thing or is it more expressive than type and set theory? In other words, does homotopic type theory really help theorem checkers/provers?

Yes. Also it includes topology.

Calling it topology can be misleading, as HoTT only considers types as spaces in the sense of homotopy equivalence.

Whether HoTT is a better foundation of mathematics (FOM) in the sense of being easier to use in practise is an open question. It's unclear even exactly what it means to be a better or worse FOM.

Note also that all well-known foundations, including HoTT are mutually relatively consistent, which amounts to being translatable into each other (so if you can derive a contradiction in one, then you can convert that into a contradiction in the other). However that is not so important in practice. Proof automation is most important for large scale reasoning. Indeed the Lean project was started with the explicit aim of bringing better proof automation to provers based on the Curry-Howard correspondence.

Homotopy Type Theory is based on Martin-Lof Type Theory (which is your standard dependent type theory), but reinterprets equality to mean homotopy equivalence. In vanilla MLTT, a = b is inhabited iff a and b share the same normal form, and its proof is refl (reflexivity). In HoTT, a = b may be inhabited by proofs other than refl. Namely, the univalence axiom states that types are equal when they are isomorphic, and function extensionality states that functions are equal when they map the same inputs to the same outputs. You also get higher inductive types, which allow you to define constructors of equalities on inductive types. So, HoTT allows you to prove things that you can't prove under ordinary MLTT.

> So, HoTT allows you to prove things that you can't prove under ordinary MLTT.

Well, adding consistent axioms often allows proving more thing, but that in itself does not necessarily mean it's more useful, and certainly not that proofs are easier -- that, I believe, was the question. For example, adding the axiom 1/0 = 0 is consistent with ordinary arithmetics, and also allows you to prove more things (e.g. that 1/0 = 0), but is not necessarily useful and not necessarily helpful.

Here's the HTML version of the same thing:

https://leanprover.github.io/theorem_proving_in_lean/

Why learn Lean as written in the book when there is no way of knowing how much of it will be obsolete in Lean 4, which is being developed in private?

Where can I read more about the decision to develop Lean 4 in private, and what is the status of https://github.com/leanprover/lean4, in your view?

Lean 4 is no longer being developed in private; this was true a year ago but is no longer true. What is true is that Lean 4 is still not ready for the port of the maths library to begin, and we do not know when it will be. Furthermore, one cannot yet use Lean 4 within VS Code, which makes it more inconvenient to use than Lean 3. But we can wait. Lean 3 is good enough to do a lot of modern mathematics so it seems, and the community are happy to work with Lean 3 currently.

How would you compare the state of proof automation to be expected from Lean 4 in comparison with Isabelle/HOL? I'm quite familiar with the latter.

Because the book is a great introduction to theorem proving in general. All those concepts learned translate nicely to other theorem provers, and especially Lean 4.

Lean 4 has already gone public: https://github.com/leanprover/lean4/

Also, afaik it won't differ from Lean 3 to the degree where learning Lean 3 is useless.

There is every way of knowing how much will be obsolete in Lean 4, as long as you're following the discussions at https://leanprover.zulipchat.com . The type theory of Lean 4 will be the same as Lean 3, there are some minor syntax changes and conventions for variable naming have changed from this_way to ThatWay but all the type theory is the same and the book will be an excellent introduction to Lean 4.

The main issue with Lean 4 is that there is currently no tactic state, but the designer Leo de Moura is currently hard at work at this, because they need tactics to start work on their IMO Grand Challenge https://imo-grand-challenge.github.io/ . Even when tactics are done, there will be no type class inference so the port of the maths library from Lean 3 to Lean 4 will probably not begin then. Type class inference is a complex issue and some of the chat on the zulip chat is about issues that users have been having in Lean 3 and how they might be fixed in Lean 4. But, in short, the basic principles are all the same. In short, I would thoroughly recommend this book.

A discussion from last year: https://news.ycombinator.com/item?id=17171101

has anybody proved something interesting in Lean? Perhaps not too difficult, but some proposition that might take a couple of days of work done in hours? I'm all for encoding foundations in a programmatic framework, but it seems that the idea here is to make this a useful tool for practicing mathematicians. The documentation didn't seem to have any examples of how that might happen.

It's also a useful tool for practising programmers as well!

The documentation for it isn't so great but Lean is a fully dependently typed programming language with a good VM. It is optimized for interactive theorem proving which means the type checker is really fast. I think getting a good native compiler out of it is not far off.

Well, there is the entire mathematical components library[0]. It's still fairly elementary, roughly at an advanced undergraduate level.

Right now it actually takes far more time to write lean code than to prove things by hand. What is typically done in a single lecture in an intro Algebraic Number Theory course can take hours upon hours to implement. E.g. the Pell equation [1]. You have to be extremely explicit about everything, and can't handwave the details you do in human proofs.

Right now the overhead of writing proofs in Lean is so large that you'd prove a theorem with pen and paper before attempting it in Lean. So far it is a useful tool for proof verification, but not for actually coming up with them.

As things stand, computer proofs are only better than humans for things that are highly combinatorial in nature. which due to performance concerns usually aren't written in languages running in VMs.

[0]https://github.com/leanprover-community/mathlib

[1]https://github.com/leanprover-community/mathlib/blob/master/...

As someone who's never used Lean, but has played around with Coq and Agda, how do they compare?

I've used Lean a fair bit (mostly contributing to mathlib), and have had a cursory glance at Coq. They are pretty similar, with really similar foundations. Both use variants of Calculus of Inductive Constructions for their foundation. Syntactically, Lean seems neater than Coq, and has more flexible pattern matching, and type inference.

It also has inbuilt support for quotient structures, which is a huge timesaver when dealing with Algebra. Might not be so important if you want to prove the correctness of programs. But I think the main advantage is that Lean is it's own meta-programming language, so you don't need to switch to Ltac/OCaml to write tactics.

The main advantage Coq has is it's code extraction feature. There was talk about implementing code extraction to C++ in Lean, but I don't think it has been done yet.

An oversimplified summary would be that Coq was designed with programmers in mind, while Lean was designed with mathematicians.

It's notable, that Coq has more libraries and useful extensions. And they merged Ltac2 into the master, so tactics writing should be better soon.

related: https://news.ycombinator.com/item?id=21107706 - Number theorist fears many proofs widely considered to be true are wrong (vice.com)

Reply on news.ycombinator.com