Lean for the Curious Mathematician YouTube Examples

Stream: Lean for the curious mathematician 2020

[Andrey Rukhin]

I am trying to follow the example found here: https://leanprover.zulipchat.com/#narrow/stream/238830-Lean-for.20the.20curious.20mathematician.202020/topic/Zoom/near/203703811

Am I correct to assume that the code as presented will not work in 2021? E.g., 'fact N + 1' is now 'factorial N + 1'. The variable 'a' is not identifiable in line 24. I cannot get that script to compile as presented.

[Scott Morrison]

Here's the current version:

import data.nat.prime
import tactic.linarith

open nat
open_locale nat

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

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

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

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

[Bjørn Remseth]

I started checking out Lean last weekend, and I've looked at the "infinitude of primes - a Lean theorem prover" demo. As a way to get started and ensure that my tooling is working I'm working through this example in visual studio code while watching the video. ... and that led me to a problem early on (see screenshot). Screenshot-2021-06-22-at-18.56.20.png

(I did initialize a lean project in a new directory using the "leanproject new infinitude_of_primes" command, and then I opened the directory in code before starting to edit the .lean file)

It seems like I've done a silly mistake that stops '+' from doing what it is intended to do, but being a beginner I don't know what that mistake is.

Any suggetions about what I'm doing wrong?

[Patrick Massot]

Lean thinks you're talking about another fact (one that means fact, not factorial)

[Kevin Buzzard]

The error says "fact N is a proposition, you can't add something to that!". This is because since that video, we have a second usage of fact in the library and in fact factorial might be renamed now?

[Kevin Buzzard]

Yes, fact is now called factorial (and has notation ! if you open_locale nat)

[Kevin Buzzard]

That's a shame, that a video which people come across has some Lean code which no longer compiles, but I guess that's just life.

[Bjørn Remseth]

Okay. I'm no longer confused :-) Thank you again.

[Patrick Massot]

The GitHub repository of this workshop is still updated but unfortunately we can't update the videos.

[Bjørn Remseth]

I see. The video was nice though (added a comment in youtube)

[Sara Díaz Real]

Hello! I have formalized a problem from the International Mathematical Olympiad (IMO) as part of my master's degree and I would like to include it at the next repository on GitHub: https://github.com/leanprover-community/mathlib/tree/master/archive/imo. Can someone explain to me how to do it? Thank you very much!

[Johan Commelin]

@Sara Díaz Real This youtube video explains it quite well: https://www.youtube.com/watch?v=Bnc8w9lxe8A

[Kevin Buzzard]

Hey that's great to hear! This message is not really in the right stream. The best way to do it would be to ask in #general for push access to non master branches of mathlib and give your github username and tag @ maintainers . Then clone mathlib with leanproject get mathlib and add your file to the archive/imo directory and submit a pull request. Feel free to ask more questions if you need any details for any of the parts of this workflow.

[Sara Díaz Real]

Thank you very much! It is the first time I use zulip so I didn't know how to use it quite well, sorry. I will try to do it in the next few days and I hope it will work!!