Joel McCracken

Stream: new members

[Joel McCracken]

Hi, My name is Joel. I'm a professional Haskell developer, and have been growing my interest in Lean and mathematics in general.

[Joel McCracken]

as I study deeper topics in CS and PLT especially, I run into problems where my lack of training in proving things is limiting my ability to understand the material. So, I've been working on that. I'm slowly working through Velleman's How to Prove It, but I naturally wish I had a way to check my proofs, as I have no idea if my proof is correct (or not).

What I'd like to do is use Lean for this, but I've been having some trouble getting started with it and understanding how bits and pieces fit together. So, as a way to resolve that, I started looking at the learning resources for lean, with the goal of starting with some simpler proofs and building from there. So, I started reading https://leanprover.github.io/logic_and_proof/index.html

However, I found that one of the very first examples:
https://leanprover-community.github.io/lean-web-editor/#code=import%20data.nat.prime%0Aopen%20nat%0A%0Atheorem%20sqrt_two_irrational%20%7Ba%20b%20%3A%20%E2%84%95%7D%20(co%20%3A%20gcd%20a%20b%20%3D%201)%20%3A%0A%20%20a%5E2%20%E2%89%A0%202%20*%20b%5E2%20%3A%3D%0Aassume%20h%20%3A%20a%5E2%20%3D%202%20*%20b%5E2%2C%0Ahave%202%20%E2%88%A3%20a%5E2%2C%0A%20%20by%20simp%20%5Bh%5D%2C%0Ahave%202%20%E2%88%A3%20a%2C%0A%20%20from%20prime.dvd_of_dvd_pow%20prime_two%20this%2C%0Aexists.elim%20this%20%24%0Aassume%20(c%20%3A%20nat)%20(aeq%20%3A%20a%20%3D%202%20*%20c)%2C%0Ahave%202%20*%20(2%20*%20c%5E2)%20%3D%202%20*%20b%5E2%2C%0A%20%20by%20simp%20%5Beq.symm%20h%2C%20aeq%5D%3B%0A%20%20%20%20simp%20%5Bpow_succ'%2C%20mul_comm%2C%20mul_assoc%2C%20mul_left_comm%5D%2C%0Ahave%202%20*%20c%5E2%20%3D%20b%5E2%2C%0A%20%20from%20mul_left_cancel'%20dec_trivial%20this%2C%0Ahave%202%20%E2%88%A3%20b%5E2%2C%0A%20%20by%20simp%20%5Beq.symm%20this%5D%2C%0Ahave%202%20%E2%88%A3%20b%2C%0A%20%20from%20prime.dvd_of_dvd_pow%20prime_two%20this%2C%0Ahave%202%20%E2%88%A3%20gcd%20a%20b%2C%0A%20%20from%20dvd_gcd%20%E2%80%B92%20%E2%88%A3%20a%E2%80%BA%20%E2%80%B92%20%E2%88%A3%20b%E2%80%BA%2C%0Ahave%202%20%E2%88%A3%20(1%20%3A%20%E2%84%95)%2C%0A%20%20by%20simp%20*%20at%20*%2C%0Ashow%20false%2C%20from%20absurd%20%E2%80%B92%20%E2%88%A3%201%E2%80%BA%20dec_trivial

does not currently work (this is the second example here https://leanprover.github.io/logic_and_proof/introduction.html#interactive-theorem-proving), I really don't understand the error message from the lean-web-editor. Was mathlib updated with backwards incompatible changes on the web editor or something? Can I change that? If not, can I find out which versions I need and set them up locally?

So, I guess I'm looking for some general guidance. Where do I start on this Journey?

Additionally, from what I read, while its clear that lean 4 is not backwards compatible with lean 3, based upon what I read here https://leanprover.github.io/lean4/doc/lean3changes.html, it seems that it should be relatively straightforward to translate anything written about lean 3 to lean 4?

[Kyle Miller]

Just to answer your question about the errors in the proof, here's something I got working with some renamings:

import data.nat.prime
open nat

theorem sqrt_two_irrational {a b : ℕ} (co : gcd a b = 1) :
  a^2 ≠ 2 * b^2 :=
assume h : a^2 = 2 * b^2,
have 2 ∣ a^2,
  by simp [h],
have 2 ∣ a,
  from nat.prime.dvd_of_dvd_pow prime_two this,
exists.elim this $
assume (c : nat) (aeq : a = 2 * c),
have 2 * (2 * c^2) = 2 * b^2,
  by simp [eq.symm h, aeq];
    simp [pow_succ', mul_comm, mul_assoc, mul_left_comm],
have 2 * c^2 = b^2,
  from mul_left_cancel₀ dec_trivial this,
have 2 ∣ b^2,
  by simp [eq.symm this],
have 2 ∣ b,
  from nat.prime.dvd_of_dvd_pow prime_two this,
have 2 ∣ gcd a b,
  from dvd_gcd ‹2 ∣ a› ‹2 ∣ b›,
have 2 ∣ (1 : ℕ),
  by simp * at *,
show false, from absurd ‹2 ∣ 1› dec_trivial

[Kyle Miller]

One problem is that there's now both prime and nat.prime, so I needed to fully qualify nat.prime.dvd_of_dvd_pow. The second is that mul_left_cancel' seems to have been renamed to mul_left_cancel₀.

[Kyle Miller]

I'm not sure which version of Lean & mathlib the textbook Logic and Proof is expecting, but in principle you can set up a project locally on your computer with exactly the right versions to follow along with the textbook.

[Kyle Miller]

Here's one resource to keep with with all of mathlib's backwards incompatible changes, for example https://mathlib-changelog.org/theorem/mul_left_cancel'

[Kyle Miller]

If you haven't done it already, as a very first step you could do #nng

[Joel McCracken]

Ah, thank you!

[Kevin Buzzard]

@Dan Velleman is on this server and they've been thinking about their book and Lean!

[Joel McCracken]

Oh cool, well @Dan Velleman if you did that I would certainly enjoy it =) I've been considering putting my proofs up on github when I get them.

[Dan Velleman]

Joel, you could be a guinea pig for a project I'm working on. You can find it here.

[Joel McCracken]

Oh sweet, yeah I'll totally do it. Are you open to any contributions? I was hoping to also verify some of the earlier proofs, for example these were long enough that I started to feel uncertain that I had done them correctly: Screen-Shot-2023-02-18-at-4.36.54-PM.png (from section 1.4 page 43)

[Joel McCracken]

Ah, ok, so it seems that your recommendation is to do it by hand until section 3.2. OK, I can do that

[Dan Velleman]

Eventually you will be able to do proofs like that, but they're probably not the best ones to start with.

[Dan Velleman]

A couple of warnings:

1. This is a work in progress. There may be glitches, and things may change.
2. My focus is on teaching math, not teaching Lean. So there's lots of stuff about Lean that isn't covered, and the Lean proofs look pretty different from the proofs that most Lean users write.

I'd really appreciate any feedback you can give me.

[Joel McCracken]

ok, will do! I really like your book, it has helped me get past some points I've been struggling with for a long time. I'll definitely be working though this lean adaptation of your book. Thanks!