Zulip Chat Archive

Stream: Lean for the curious mathematician 2020

Topic: Zoom


Floris van Doorn (Jul 13 2020 at 05:16):

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 (Jul 13 2020 at 06:19):

@LFTCM Hey everyone! Zoom is now open.

Johan Commelin (Jul 13 2020 at 09:29):

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 (Jul 13 2020 at 10:43):

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

Scott Morrison (Jul 13 2020 at 10:46):

(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 (Jul 13 2020 at 10:55):

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

Johan Commelin (Jul 13 2020 at 10:59):

We are starting!

Scott Morrison (Jul 13 2020 at 11:32):

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 (Jul 13 2020 at 11:35):

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 (Jul 13 2020 at 11:36):

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

Johan Commelin (Jul 14 2020 at 07:04):

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 (Jul 15 2020 at 07:45):

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 (Jul 15 2020 at 08:11):

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 (Jul 15 2020 at 08:12):

git checkout -- leanpkg.toml should hopefully fix that

Philip Vetter (Jul 15 2020 at 08:13):

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

Filippo A. E. Nuccio (Jul 15 2020 at 08:16):

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 (Jul 15 2020 at 08:17):

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

Scott Morrison (Jul 15 2020 at 08:17):

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

Johan Commelin (Jul 15 2020 at 08:17):

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

Johan Commelin (Jul 15 2020 at 08:28):

@Dima Pasechnik :up:

Chandan Sah (Jul 23 2022 at 09:35):

Hi

Chandan Sah (Jul 23 2022 at 09:36):

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 (Jul 23 2022 at 09:36):

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 (Jul 23 2022 at 09:37):

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

Mark Gerads (Jul 23 2022 at 09:45):

N needs a type (natural number)
image.png

Chandan Sah (Jul 23 2022 at 09:57):

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

Chandan Sah (Jul 23 2022 at 09:59):

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

Mark Gerads (Jul 23 2022 at 09:59):

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 (Jul 23 2022 at 10:00):

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

Chandan Sah (Jul 23 2022 at 10:01):

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

Mark Gerads (Jul 23 2022 at 10:03):

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 (Jul 23 2022 at 10:32):

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 (Jul 23 2022 at 10:33):

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 (Sep 29 2023 at 08:20):

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 (Sep 29 2023 at 08:25):

docs#Nat.exists_infinite_primes

Ming Li (Sep 29 2023 at 09:08):

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 (Sep 29 2023 at 10:43):

That is a link to mathlib4

Ming Li (Sep 29 2023 at 10:49):

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 (Sep 29 2023 at 11:19):

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 (Sep 29 2023 at 11:46):

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 (Sep 29 2023 at 12:16):

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

Ming Li (Sep 29 2023 at 13:18):

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 (Sep 29 2023 at 13:26):

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

Ming Li (Sep 29 2023 at 13:51):

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


Last updated: Dec 20 2023 at 11:08 UTC