Zoom

Stream: Lean for the curious mathematician 2020

[Floris van Doorn]

Hello everyone!

The Zoom meeting has not started yet for the install session. It will open around 9:00 AM CEST. You can join it with the link/ID and password below. This information will be posted on the website shortly.

Topic: Lean for the Curious Mathematician
Time: Jul 13, 2020 07:00 AM Amsterdam, Berlin, Rome, Stockholm, Vienna
Every day, 5 occurrence(s)
Jul 13, 2020 07:00 AM
Jul 14, 2020 07:00 AM
Jul 15, 2020 07:00 AM
Jul 16, 2020 07:00 AM
Jul 17, 2020 07:00 AM
Please download and import the following iCalendar (.ics) files to your calendar system.
Daily: https://vu-live.zoom.us/meeting/tJEpd-uopj4jGtRLTcJg_Y9FR5KHpW94me9h/ics?icsToken=98tyKuCtqjsoGtyQuRmHRowMBoiga_TxiCVEjbdvsCvmKSdsW1rQBLdpGqJISYzd

Join Zoom Meeting
https://vu-live.zoom.us/j/95402085900

Meeting ID: 954 0208 5900
Password: 333537

[Johan Commelin]

@LFTCM Hey everyone! Zoom is now open.

[Johan Commelin]

Public Service Announcement: if you don't have Zoom installed, please install it. We'll start with the first talk in about 90 minutes.

[Johan Commelin]

Hello everyone! The details for the Zoom meeting are posted in the thread. (Just scroll up a bit.)

[Scott Morrison]

(Or, in Zulip, you can always click on just the title of the thread, e.g. "Zoom" here, to read only that thread.)

[Johan Commelin]

We are starting in a couple of minutes. Please login on Zoom, if you haven't done so already.

[Johan Commelin]

We are starting!

[Scott Morrison]

For anyone who wants to inspect the proof I just wrote:

import data.nat.prime
import tactic.linarith

open nat

theorem infinitude_of_primes : ∀ N, ∃ p ≥ N, prime p :=
begin
  intro N,

  let M := fact N + 1,
  let p := min_fac M,

  have pp : prime p :=
  begin
    refine min_fac_prime _,
    have : fact N > 0 := fact_pos N,
    linarith,
  end,

  use p,
  split,
  { by_contradiction,
    have h₁ : p ∣ fact N + 1 := min_fac_dvd M,
    have h₂ : p ∣ fact N := (prime.dvd_fact pp).mpr (le_of_not_ge a),
    have h : p ∣ 1 := (nat.dvd_add_right h₂).mp h₁,
    exact prime.not_dvd_one pp h, },
  { exact pp, },
end

[Rob Lewis]

The Zoom link for the Monday afternoon metaprogramming session is:
https://vu-live.zoom.us/j/99368691219 (Password: 654479)

But I suggest watching (some of) the YouTube videos first!

[Rob Lewis]

(https://leanprover.zulipchat.com/#narrow/stream/238830-Lean-for.20the.20curious.20mathematician.202020/topic/Monday.20afternoon.3A.20metaprogramming.20session)

[Johan Commelin]

Floris van Doorn said:

Hello everyone!

The Zoom meeting has not started yet for the install session. It will open around 9:00 AM CEST. You can join it with the link/ID and password below. This information will be posted on the website shortly.

Topic: Lean for the Curious Mathematician
Time: Jul 13, 2020 07:00 AM Amsterdam, Berlin, Rome, Stockholm, Vienna
Every day, 5 occurrence(s)
Jul 13, 2020 07:00 AM
Jul 14, 2020 07:00 AM
Jul 15, 2020 07:00 AM
Jul 16, 2020 07:00 AM
Jul 17, 2020 07:00 AM
Please download and import the following iCalendar (.ics) files to your calendar system.
Daily: https://vu-live.zoom.us/meeting/tJEpd-uopj4jGtRLTcJg_Y9FR5KHpW94me9h/ics?icsToken=98tyKuCtqjsoGtyQuRmHRowMBoiga_TxiCVEjbdvsCvmKSdsW1rQBLdpGqJISYzd

Join Zoom Meeting
https://vu-live.zoom.us/j/95402085900

Meeting ID: 954 0208 5900
Password: 333537

Zoom is now open again. If you need help with some final things (e.g. involving installation) please head over there so that we can take a look (via screen sharing, for example).

[Johan Commelin]

Zoom is open again, but see the message at https://leanprover.zulipchat.com/#narrow/stream/238830-Lean-for.20the.20curious.20mathematician.202020/topic/Wednesday.20morning/near/203924848

Join Zoom Meeting
https://vu-live.zoom.us/j/95402085900

Meeting ID: 954 0208 5900
Password: 333537

[Philip Vetter]

git checkout -- , followed by git pull, still complains of changes to leanpkg.toml, which are not any changes I intended to make and don't mind losing.

[Johan Commelin]

git checkout -- leanpkg.toml should hopefully fix that

[Philip Vetter]

thanks. git stash worked, (but not really what I wanted to do)

[Filippo A. E. Nuccio]

What should we do with our local exercises? I have created a folder copied from /src in lftcm2020 but may be we don't want that all participants upload them. Should I commit and pull but never push?

[Alex J. Best]

Yes that sounds best (probably push would reject you anyway)

[Scott Morrison]

@Filippo, I would suggest never adding your local copies to git.

[Johan Commelin]

If you don't add them, git will ignore them

[Johan Commelin]

@Dima Pasechnik :up:

[Chandan Sah]

Hi

[Chandan Sah]

Scott Morrison said:

For anyone who wants to inspect the proof I just wrote:

import data.nat.prime
import tactic.linarith

open nat

theorem infinitude_of_primes : ∀ N, ∃ p ≥ N, prime p :=
begin
  intro N,

  let M := fact N + 1,
  let p := min_fac M,

  have pp : prime p :=
  begin
    refine min_fac_prime _,
    have : fact N > 0 := fact_pos N,
    linarith,
  end,

  use p,
  split,
  { by_contradiction,
    have h₁ : p ∣ fact N + 1 := min_fac_dvd M,
    have h₂ : p ∣ fact N := (prime.dvd_fact pp).mpr (le_of_not_ge a),
    have h : p ∣ 1 := (nat.dvd_add_right h₂).mp h₁,
    exact prime.not_dvd_one pp h, },
  { exact pp, },
end

@Scott Morrison When I type the 3rd line out it shoes the following error message

[Chandan Sah]

Error updating: Error fetching goals: {"stack":"Error: Incorrect position 'file:///c%3A/Users/Aadarsh%20Sah/Documents/Codes_VS/lean4-samples/HelloWorld/Main.lean:3:0' in RPC call\n\tat c:\\Users\\Aadarsh Sah\\.vscode\\extensions\\leanprover.lean4-0.0.85\\dist\\extension.js:2:550160\n\tat c:\\Users\\Aadarsh Sah\\.vscode\\extensions\\leanprover.lean4-0.0.85\\dist\\extension.js:2:550454\n\tat Immediate.<anonymous> (c:\\Users\\Aadarsh Sah\\.vscode\\extensions\\leanprover.lean4-0.0.85\\dist\\extension.js:2:550816)\n\tat processImmediate (node:internal/timers:464:21)","message":"Incorrect position 'file:///c%3A/Users/Aadarsh%20Sah/Documents/Codes_VS/lean4-samples/HelloWorld/Main.lean:3:0' in RPC call","code":-32602}

[Chandan Sah]

It also gives output message saying "unknown package 'data'"
How to add this "data" package then? @Scott Morrison

[Mark Gerads]

N needs a type (natural number)
image.png

[Chandan Sah]

I didnt understand what you suggest me to do @Mark Gerads

[Chandan Sah]

My question is "how to download the data package?"

[Mark Gerads]

Well, You have an error with Lean4, so maybe that is why it did not work for me. I am using Lean3. I was showing you a screenshot of my error.

[Mark Gerads]

I was under the impression that Lean3 was easier to set up than Lean4. Is there a reason to not use Lean3?

[Chandan Sah]

I installed lean4 just because it is the newer version but now c0me to realize that it has got errors

[Mark Gerads]

Okay. Lean4 is still considered experimental, Lean3 is the stable release. I suggest trying Lean3 https://leanprover-community.github.io/get_started.html

[Damiano Testa]

Chandan, as you are finding out, Lean3 and Lean4 are incompatible. Moreover, old versions of mathlib are usually also incompatible with newer versions! This is an adaptation (still in Lean 3, but with the current mathlib) of Scott's code above:

import data.nat.prime
import tactic.linarith

open nat
open_locale nat

theorem infinitude_of_primes : ∀ N : ℕ, ∃ p ≥ N, p.prime :=
begin
  intro N,

  let M := N! + 1,
  let p := M.min_fac,

  have pp : p.prime :=
  begin
    refine nat.min_fac_prime _,
    have : N! > 0 := N.factorial_pos,
    linarith,
  end,

  use p,
  split,
  { by_contradiction,
    have h₁ : p ∣ N! + 1 := M.min_fac_dvd,
    have h₂ : p ∣ N! := nat.dvd_factorial pp.pos (not_le.mp h).le,
    have h : p ∣ 1 := (nat.dvd_add_right h₂).mp h₁,
    exact pp.not_dvd_one h },
  { exact pp, },
end

I used dot-notation more extensively, which is maybe not ideal pedagogically, but since now there are prime and nat.prime, simply writing prime is more ambiguous.

[Damiano Testa]

Note also the notation N! that likely did not exist when Scott wrote this demo and that is available if you use open_locale nat before you want to use it.

[Ming Li]

Is there any version in Lean4 now?
Damiano Testa said:

Chandan, as you are finding out, Lean3 and Lean4 are incompatible. Moreover, old versions of mathlib are usually also incompatible with newer versions! This is an adaptation (still in Lean 3, but with the current mathlib) of Scott's code above:

import data.nat.prime
import tactic.linarith

open nat
open_locale nat

theorem infinitude_of_primes : ∀ N : ℕ, ∃ p ≥ N, p.prime :=
begin
  intro N,

  let M := N! + 1,
  let p := M.min_fac,

  have pp : p.prime :=
  begin
    refine nat.min_fac_prime _,
    have : N! > 0 := N.factorial_pos,
    linarith,
  end,

  use p,
  split,
  { by_contradiction,
    have h₁ : p ∣ N! + 1 := M.min_fac_dvd,
    have h₂ : p ∣ N! := nat.dvd_factorial pp.pos (not_le.mp h).le,
    have h : p ∣ 1 := (nat.dvd_add_right h₂).mp h₁,
    exact pp.not_dvd_one h },
  { exact pp, },
end

I used dot-notation more extensively, which is maybe not ideal pedagogically, but since now there are prime and nat.prime, simply writing prime is more ambiguous.

[Kevin Buzzard]

docs#Nat.exists_infinite_primes

[Ming Li]

Thanks. I am using Lean 4 and mathlib4. So the source code does not go through.

Kevin Buzzard said:

docs#Nat.exists_infinite_primes

[Kevin Buzzard]

That is a link to mathlib4

[Ming Li]

Sorry, it said "unexpected token '+'; expected term" for "minFac (n ! + 1)". How to fix it?
On the top of the source code, there is the information #align_import data.nat.prime from "leanprover-community/mathlib"@"8631e2d5ea77f6c13054d9151d82b83069680cb1". It seems it is not available anymore...

Kevin Buzzard said:

That is a link to mathlib4

[Damiano Testa]

Using VSCode, if in an empty file I write

import Mathlib.Data.Nat.Prime

#check Nat.exists_infinite_primes

and right-click on Nat.exists_infinite_primes to "Go to definition", VSCode takes me to the right place and everything compiles.

[Ming Li]

Thanks. I am using VSCode too. It did go through. However, I prefer to show my students how to access the LEAN code, after I proved the result on blackboard.

[Damiano Testa]

Maybe I am missing something, but "Go to definition" should take you to the Lean code for the result.

[Ming Li]

I got it. Thanks a lot. The code is much longer than I expect. I am not sure students can accept it with patience. LOL

[Damiano Testa]

It is certainly true that, at least currently, formalization is much more verbose than informal maths!

[Ming Li]

I thought mathematicians have done quite well on formalization and formal proof.