Polya / Goldbach Proof for Infinite Primes in Lean?

Stream: new members

[North Eastern Ohio Mac Developer]

Hi,

I am very new to Lean, and am trying to learn by figuring out how to properly write some classic proofs in Lean. The one I am currently attempting is the classic Polya / Goldbach proof for the infinitude of primes.

This classic proof first involves first proving that any two Fermat numbers are relatively prime. (Feel free to leave that out-of-scope for this question.) Assuming Fermat numbers being relatively prime is already done, how would one represent the core idea of the Polya / Goldbach proof for the infinitude of primes as expressed in English below in Lean?

There are infinitely many distinct Fermat numbers, each of which is divisible by an odd prime, and since any two Fermat numbers are relatively prime, these odd primes must all be distinct. Thus, there are infinitely many primes.

[Ruben Van de Velde]

Do you have a #mwe of the theorem you're proving already?

[Daniel Weber]

Here's how I would go about it:

• Construct the set of Fermat numbers as {2 ^ (2 ^ n) + 1 | n}, and show that it's infinite
• Consider Nat.minFac '' {2 ^ (2 ^ n) + 1 | n}. By docs#Nat.minFac_prime it's a subset of the set of primes, so it suffices to show that it's infinite by docs#Set.Infinite.mono
• Using docs#Set.Infinite.image, it suffices to show that docs#Nat.minFac is injective on the set of Fermat numbers.
• Let there be two Fermat primes with equal Nat.minFac. It divides both of them, so they aren't coprime, so they must be equal.

[North Eastern Ohio Mac Developer]

@Daniel Weber Thank you for the reply. I'm sure someone more experienced in Lean might understand your response, but sadly it doesn't mean anything to me. My total experience with Lean so far is only about 40 hours -- over 10 hours of which was just figuring out how to get the Hello World to include MathLib. (As an aside in my 25+ years as a coder, I've found the Lean docs the worst getting started experience of any language I've ever used so far.)

At any rate, I understand how the proof typically is done (first prove recurrence relation, then prove all Fermat numbers are relatively prime, then because there are infinite Fermat numbers there must be infinite primes), but I am just struggling with how to express any of it in actual Lean statements.

For example, I understand how to write a function for a Fermat number. (Although I still don't understand why I have to write "Nat" when I see that fancy N symbol for the natural numbers in many examples on-line, but that doesn't work for me when copied & pasted.)

def Fermat (n : Nat) : Nat := 2^(2^n) + 1

Then I first start trying to write a statement for a theorem for the Fermat recurrence relation, but after spending most of the day today googling and reading docs I haven't even figured out how to successfully write the first line -- just how to express the recurrence relation on the first "theorem" line. Below I have it written out as a list of products with a ... in the middle until I can figure out how to enter it properly. For example, I see examples online with the epsilon & pi symbol, but when I copy them into my code they don't work nor could I figure out any way to enter those characters without copying & pasting from a website. I read lots of docs about "finset.prod" but was never able to figure out how to ever enter a Lean statement that successfully used it.

/-- Prove Fermat(n+1) - 2 = Fermat(0) * Fermat(1) * ... * Fermat(n-1) * Fermat (n) -/
theorem FematRecurrence { n : Nat } : Fermat (0) * Fermat (1) * ... * Fermat (n-1) * Fermat (n) = Fermat (n+1) - 2 :=
-- Start with 1 times the product, 1 represented as (2^2^0-1)
-- (2^2^0-1)*(2^2^0+1)*(2^2^1+1)*...*(2^2^n+1)
-- Repeatedly collapse the first two terms of the product sequence until only two terms remain
-- (2^2^1-1)*(2^2^1+1)*(2^2^2+1)*...*(2^2^(n-1)+1)*(2^2^n+1)
-- (2^2^2-1)*(2^2^2+1)*...*(2^2^(n-1)+1)*(2^2^n+1)
-- (2^2^3-1)*(2^2^3+1)*...*(2^2^(n-1)+1)*(2^2^n+1)
-- ...
-- (2^2^n-1)*(2^2^n+1)
-- 2^2^(n+1)-1
-- Rewrite -1 as +1-2
-- 2^2^(n+1)+1-2
-- 2^2^(n+1)+1 is Fermat(n+1) thus
-- Fermat(n+1)-2
begin
  induction n,
  -- Base case: n = 0
  case n.zero =>
    show Fermat (0) == Fermat (1) - 2 := by simp,
  -- Induction
  case n.succ =>
-- ???
end

I haven't even really gotten so far as trying to figure out how to write the induction step yet. I've been hung up all day on just figuring out how to write the first theorem line properly for the product.

[Benjamin Jones]

Here's some syntax and definitions help:

import Mathlib.Algebra.BigOperators.Group.Finset
import Mathlib.Data.Finset.Basic
import Mathlib.Tactic

open Finset  -- brings in scope names of lemmas and defs related to finite sets

def Fermat (n : Nat) : Nat := 2^(2^n) + 1

#check Finset.prod
#check Finset.range
-- For more, look at the documentation at the top of `Mathlib/Data/Finset/Basic.lean` file

-- Here's a start on your recurrence
theorem FermatRecurrence {n : Nat} : Finset.prod (range (n+1)) (fun i => Fermat i) = Fermat (n+1) - 2 := by
  induction' n with k ih
  · simp only [zero_add, range_one, prod_singleton]
    unfold Fermat
    norm_num
  · -- use relationship b/w range (k+1) and range (k + 1 + 1)
    sorry

-- Here's the same statement, but using "big operators"
theorem FermatRecurrence' {n : Nat} : ∏ i ∈ range (n+1), Fermat i = Fermat (n+1) - 2 := by
  sorry

To understand better what's going on here, working through https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html would be very useful. Especially Ch. 5 which develops several alternate proofs of the infinitude of primes. That chapter also shows you how to work with finite sets and regular/strong induction.