Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Theorem Proving in Lean [pdf]

leanprover.github.io

Post reply on HN
Print view View original

11–20 of 23 posts

Re: Theorem Proving in Lean [pdf]

#11

Post by kevinzz »

jbapple wrote: post #5
iso-8859-1 wrote: post #4

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.

Re: Theorem Proving in Lean [pdf]

#12

Post by mafribe »

kevinzz wrote: post #11
jbapple wrote: post #5

Earlier quoted context omitted.

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…

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.

Re: Theorem Proving in Lean [pdf]

#14

Post by TheAsprngHacker »

The_rationalist wrote: post #7
p0llard wrote: post #3

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'…

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?

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.

Re: Theorem Proving in Lean [pdf]

#15

Post by TheAsprngHacker »

adamnemecek wrote: post #8
The_rationalist wrote: post #7

Earlier quoted context omitted.

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.

Re: Theorem Proving in Lean [pdf]

#16

Post by comnetxr »

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.

Re: Theorem Proving in Lean [pdf]

#17

Post by dpah »

TheAsprngHacker wrote: post #13

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.

Re: Theorem Proving in Lean [pdf]

#19

Post by xvilka »

dpah wrote: post #17
TheAsprngHacker wrote: post #13

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 whe…

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.

Re: Theorem Proving in Lean [pdf]

#20

Post by agentultra »

comnetxr wrote: post #16

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.

Post reply on HN