Doing a math assignment with the Lean theorem prover(ahelwer.ca)

141 pointsby ahelwer6 anni fa29 comments

Doing a math assignment with the Lean theorem prover

https://ahelwer.ca/post/2020-04-05-lean-assignment/

7 comments

xvilka6 anni fa

The same can be done also with Coq[1], it is easy to learn[2], actively developed[3], and better documented[4]. You can also visit their discussion board[5]. Regarding the usual Lean vs Coq "war" and so-called "setoid hell" you can read a lengthy discussion on their GitHub[6].

[1] http://coq.inria.fr/

[2] https://learnxinyminutes.com/docs/coq/

[3] https://github.com/coq/coq

[4] https://softwarefoundations.cis.upenn.edu/

[5] https://coq.discourse.group/

[6] https://github.com/coq/coq/issues/10871

ahelwer6 anni fa

I tried learning Coq through the Software Foundations track a couple times and enjoyed what I did learn, but bounced off. If Coq made something similar to the Natural Number Game [0] I'd love to give it a go and see the differences!

[0] https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...

ivanbakel6 anni fa

That final link is very insightful. Not to pick sides, but if Lean really doesn't have subject reduction when you use quotient types, that's a crazy property to drop (or lose accidentally).

ocfnash6 anni fa

I have a little experience of both Coq and Lean and have followed some of the discussion about Lean's handling of quotient types.

I have seen computer scientists emphasise to mathematicians that subject reduction should not be forfeit but I have yet to see a convincing argument/example for why not.

I don't suppose you can elaborate on why this may be / is so crazy, that someone with only a limited understanding of type theory might follow?

zozbot2346 anni fa

Setoids are also very relevant in constructive math, for similar reasons. Quotient types/sets basically conflate cases where one can easily normalize the elements of some equivalent class vs. cases where this cannot be done effectively, and that's not a good approach at all.

kevinbuzzard6 anni fa

Lean's maths library development is essentially completely focussed on classical mathematics, which is why it has been so successful in drawing "working mathematicians" in. Such people do not care at all about the issues involving quotients, indeed quotients in Lean work just fine for them, and they don't care about constructibility either, because this is the prevailing culture in maths departments (although it is not, I am well aware, the prevailing culture in computer science departments). If you are interested in constructivism I would not recommend Lean. Many of the developments in mathlib are classical. That's why it's moving so quickly -- classical mathematics is much easier.

The_rationalist6 anni fa

What about coq vs z3 ? It seems they are the two most actively developed theorem provers/checkers

aweinstock6 anni fa

For a concrete example of how z3 differs from Coq, consider trying to prove that "for all integers x, there exists an integer y greater than x such that x divides y" (a subgoal of Euclid's theorem on there being infinitely many primes).

Here's a transcript of using the z3 python bindings to ask for a proof:

    $ python
    >>> import z3
    >>> x, y = z3.Ints('x y')
    >>> s = z3.Solver()
    >>> s.add(z3.Not(z3.ForAll([x], z3.Exists([y], z3.And(y >= x, y % x == 0)))))
    >>> s.check()
    unknown

z3 returns unknown (if it had returned "unsat", it would have been possible to extract a resolution-refutation proof), and there's not much that can be done with the unknown.

Here's a Coq interactive session that proves most of the cases (with one subproof left unsolved, it was taking me too long relative to the rest of the proof).

    $ coqtop
    Require Import NArith.
    Require Import Omega.

    Lemma x_le_fact : forall x, x <= fact x.
    induction x;.
    - simpl; omega.
    - simpl; admit. (* Proving `x <= fact x -> S x <= fact x + x * fact x` left unsolved here *)
    Admitted.

    Goal forall (x : nat), exists (y : nat), y >= x /\ Nat.modulo y x = 0.
    intros x; exists (fact x).
    split.
    - unfold ">=". apply x_le_fact.
    - induction x.
        + simpl; reflexivity.
        +
      (* goal here is `fact (S x) mod S x = 0` *)
      unfold fact; fold fact.
      (* goal here is `(S x * fact x) mod S x = 0` *)
      rewrite (Nat.mul_comm (S x) (fact x)).
      (* goal here is `(fact x * S x) mod S x = 0` *)
      apply (Nat.mod_mul (fact x) (S x)).
      discriminate.
    Qed.

Unlike z3, you need to manually tell Coq what the steps are, but it gives you feedback on which steps are correct, and what assumptions are available and what subgoals still remain at each step (I've included some of those as comments, running the proof through the interpreter shows more detail).

ahelwer6 anni fa

Z3 is very different from Coq and Lean. Coq and Lean are interactive theorem provers, while Z3 is a satisfiability modulo theories (SMT) solver which can do things like checking whether a logical formula is satisfiable or finding a solution for a system of constraints.

The_rationalist6 anni fa

Thanks! And what about agda and Idris?

aweinstock6 anni fa

Agda and Idris are the same sort of tool (total dependently typed languages/proof assistants/interactive theorem provers) as Lean and Coq.

umvi6 anni fa

Can someone explain why I would ever want to use Coq? Is it mainly for algorithm researchers?

agentultra6 anni fa

If you're a practicing programmer you may want to use a theorem prover like Coq or Lean for a couple of reasons:

1. You want to verify your algorithms, data structures, and properties are correct with regards to their specifications. For example: an OS micro-kernel, verified compiler, etc.

2. You want to derive some code with verified properties or deeply embed specifications. A lock-free and fair scheduler, an algorithm for sharing data that guarantees it doesn't leak private information, a real-time control system, etc. For an example of such a library see [0].

If you're a computer scientist you're probably more concerned with the first and proving more of your own theorems.

If you're a mathematician you're (probably) more interested in new theorems (I'm not a pure mathematician, I can only speculate from what I've heard Buzzard and other mathematicians say).

[0] https://hackage.haskell.org/package/containers-verified

logicchains6 anni fa

For people interested in using Lean, note that there's a community fork (https://github.com/leanprover-community/lean) of the last official Lean 3 release 3.4.2 (https://github.com/leanprover/lean). The fork is still under active maintenance, so might be a better place to start (the main development team have moved onto developing Lean 4.0 (https://github.com/leanprover/lean4), and it's not clear when that will be ready).

abjKT26nO86 anni fa

It's a bit ironic, but the author repeated the same error every time they wrote the formula involving sigma. What they wanted to write was $\sum_{0}^{n} k$. What they actually wrote ($\sum_{0}^{n} n$) is equal to $n \cdot (n+1)$ (without the division by 2).

mkl6 anni fa

Yes, though it's better to define k: $\sum_{k=0}^n k$.

ahelwer6 anni fa

lol oops, fixed thanks!

outlace6 anni fa

I just started learning Lean today - what a coincidence. I have found learning lean difficult but gratifying. The post serves as further motivation.

dhosek6 anni fa

It's a pity that the author's high school didn't use geometry as the means of introducing the concept of mathematical proof. The classical high school two-column proof is in many ways quite similar to the methods of Lean, albeit with a different structure.

Smaug1236 anni fa

I greatly recommend Lockhart's Lament (https://www.maa.org/external_archive/devlin/LockhartsLament....) which says exactly the opposite.

I didn't personally undergo "two-column proof" education, and learned what the phrase means from Lockhart's Lament itself, but it sounds miserable; I say this as an MMath who specialised in set theory and logic, and who has been side-project formalising maths in Agda for the last two years.

JadeNB6 anni fa

> I didn't personally undergo "two-column proof" education, and learned what the phrase means from Lockhart's Lament itself, but it sounds miserable; I say this as an MMath who specialised in set theory and logic, and who has been side-project formalising maths in Agda for the last two years.

As a professional mathematician who did go through two-column proof, you're not the only one who finds them miserable. Personally, abstract algebra was what won me over to the beauty of proof (probably that old standby, the irrationality of sqrt(2), was the first); but everyone will find a different experience.

dhosek6 anni fa

Aesthetically, two-column proofs are miserable, but they have the advantage that the logic is very clearly laid out. There's no chance to hand-wave when every step of the proof needs to be explicitly justified.

0az6 anni fa

I personally credit my own geometry education, as much as I disliked it, with giving me the tools I needed to succeed in Calculus. That Calculus final involved proving part two of the FTC. Fun times.

AP Calculus? It's much less helpful, in its computational focus.

aadams6 anni fa

Will you provide links?

lordnacho6 anni fa

Does Lean allow you to put in geometric proofs? Say someone draws some circles and some lines and wants to prove that some property of the intersection points is true, eg that are always on the same straight line?

h91wka6 anni fa

Quick search reveals that some people have encoded Euclid's axioms in Coq (Lean and Coq are based on roughly the same theory):

http://geocoq.github.io/GeoCoq/

wwarner6 anni fa

This is really futuristic. Feels like it could be applied to model based design.

masteranza6 anni fa

The example the author provided is too trivial to convince me to use lean.

kevinbuzzard6 anni fa

[Here](https://arxiv.org/abs/1907.01449) is a Lean formalisation of a 2017 Annals of Mathematics paper.