Infinite Fermat pseudoprimes to any base

Stream: maths

[Niels Voss]

I proved that there are an infinite number of Fermat pseudoprimes to any base starting at 1.
Here are the definitions and type signature of my proof:

def probable_prime (n : ℕ) (b : ℕ) : Prop := n ∣ b^(n - 1) - 1
def fermat_psp (n : ℕ) (b : ℕ) : Prop := nat.coprime n b ∧ probable_prime n b ∧ ¬nat.prime n ∧ n > 1
theorem exists_infinite_pseudoprimes (b : ℕ) (h : b ≥ 1) (m : ℕ) : ∃ n : ℕ, fermat_psp n b ∧ n ≥ m

The full proof (including some documentation) can be found here: https://github.com/osbourn/fermat-pseudoprimes/blob/master/src/fermat_psp.lean

I had a few questions about the proof. I was wondering if the definition for pseudoprime was set up correctly. A textbook I have states that n being coprime with b is a requirement for n to be pseudoprime, but other sources don't seem to include this requirement.
Additionally, because probable_prime was defined using divisibility instead of congruences, all numbers are probable primes to base 0 and 1, and 0 and 1 are probable primes to any base.
This definition for pseudoprime also permits a few pseudoprimes that might be considered trivial. For example, all composite numbers are pseudoprimes to base 1, and 4 is pseudoprime to base 5.

A few other questions I had were:

• Should the order of the parameters n and b be swapped? Currently fermat_psp 341 2 means 341 is a pseudoprime to base 2 but I can see the advantages of swapping them.
• Would it have been better to have used modular arithmetic instead of divisibility in the definition?
• My proof contains a variety of lemmas which are unrelated to pseudoprimes. Where should I place them?
• psp_from_prime, psp_from_prime_psp, and psp_from_prime_gt_p are all marked private because I didn't think they had much use outside of proving exists_infinite_pseudoprimes. Should they be marked private?

[Kevin Buzzard]

Whether you want n to be coprime with b might depend on whether you're using b^(n-1)-1 or b^n-b. I can believe that there is inconsistency, you might just want to go with whatever it says on Wikipedia. The definition wasn't really designed for edge cases, I wouldn't worry too much about what happens when b is small. People are going to complain if 341 isn't a pseudoprime base 2 but nobody is going to complain if your edge cases are a bit different to their edge cases because it's not the point of the definition. I think the order is fine, it's the order that they are in when we say the phrase in English. For definitions, you reap what you sew. If you've got your definition working then I wouldn't worry. If you want the definition to be equivalent to a statement using modular arithmetic then just prove that statement and give a docstring explaining why it's there.

[Kevin Buzzard]

Lemmas going elsewhere -- which lemmas in particular are you talking about? Link to the permalinks or paste the statements to stop people having to second guess you. Lemmas involving nat subtraction or division always give me pause because they all seem to me to be mathematically unnatural -- if I want to mathematically subtract naturals I would switch to integers. It's your project, you can mark whatever you like as private.

[Niels Voss]

One thing I didn't realize when I posted yesterday was that the condition n ∣ b^(n - 1) - 1 actually implies that n and b are coprime. I removed the requirement that n and b are coprime from the definition of fermat_psp and added the following two lemmas:

lemma coprime_of_probable_prime (n b : ℕ) (h : probable_prime n b) (h₁ : n ≥ 1) (h₂ : b ≥ 1) : nat.coprime n b
lemma coprime_of_fermat_psp (n b : ℕ) (h : fermat_psp n b) (h₁ : b ≥ 1) : nat.coprime n b

I apologize for not being clear when I talked about the extra lemmas. I had to prove the following statements that were unrelated to pseudoprimes for use in my proof:

lemma diff_squares (a b : ℕ) (h : a ≥ b) : (a + b) * (a - b) = a*a - b*b
lemma not_dvd_of_not_dvd_mul (a b c : ℕ) (h : ¬a ∣ b * c) : ¬a ∣ b
lemma mul_self (n : ℕ) : n * n = n ^ 2
lemma pow_factor (a b : ℕ) (h : b ≥ 1) : a^b = a * a^(b - 1)
lemma odd_of_prime_gt_two (p : ℕ) (h : nat.prime p) (hp : p > 2) : ¬2 ∣ p
lemma odd_pow_lem (a : ℤ) (n k : ℕ) (h₁ : k ∣ n) (h₂ : odd (n / k)) : a^k + 1 ∣ a^n + 1
lemma ab_lem (a b n : ℕ) : (a - b) ∣ (a^n - b^n)
lemma coprime_dvd_succ (a b : ℕ) (h : a ∣ b + 1) : nat.coprime a b
lemma pow_gt_base (a b : ℕ) (ha : a > 1) (hb : b > 1) : a^b > a
lemma pow_gt_exponent (a b : ℕ) (h : a ≥ 2) : a^b > b
lemma gt_of_sub_le (n m k l : ℕ) (h : n > m) (h₁ : k ≤ l) (h₂ : m ≥ l) : (n - k > m - l)

These statements have proofs of various length, available here:
https://github.com/osbourn/fermat-pseudoprimes/blob/53f3f7e5c54a42a63895909c7f4b22871671eb1b/src/fermat_psp.lean#L135
For the most part the names are temporary and need to be changed to become more descriptive. Some of the lemmas (like mul_self and pow_factor) I probably could have found in mathlib if I looked hard enough, but library_search didn't return anything. Yesterday I was primarily asking that if I decide to PR this to mathlib, should these lemmas should go in the same file as the rest of the proofs and definitions or some other file?

Using natural numbers instead of integers may or may not have been a mistake, since it made some of the proofs harder and it took much longer to prove inequalities involving subtraction (considering my proofs are probably already long since I am relatively new to lean). Natural numbers were also what caused the "all composite numbers are pseudoprime to base 0" edge case. If I decide to PR this to mathlib, would trying to switch to ints be better?

[Yaël Dillies]

@Mantas Baksys can tell you where odd_pow_lem and ab_lem are. For the other ones, there's docs#sq_sub_sq, docs#dvd_mul_of_dvd_left (+ docs#mt), docs#sq, docs#pow_succ

[Niels Voss]

sq_sub_sq seems to work for integers, but not for natural numbers. Is this because nat isn't a comm_ring?

[Yaël Dillies]

Yes exactly! So instead you have docs#nat.sq_sub_sq

[Niels Voss]

Using the lemmas Yaël Dillies suggested, I was able to get rid of most of the lemmas, with a few left over:

lemma odd_of_prime_gt_two (p : ℕ) (h : nat.prime p) (hp : p > 2) : odd p
lemma odd_pow_lem (a : ℤ) (n k : ℕ) (h₁ : k ∣ n) (h₂ : odd (n / k)) : a^k + 1 ∣ a^n + 1
lemma ab_lem (a b n : ℕ) : (a - b) ∣ (a^n - b^n)
lemma pow_gt_base (a b : ℕ) (ha : a > 1) (hb : b > 1) : a^b > a
lemma pow_gt_exponent (a b : ℕ) (h : a ≥ 2) : a^b > b

I think I might be able to eliminate odd_of_prime_gt_two and pow_gt_base soon, since those are less complicated than the others.
I also added an extra lemma to help convert between the divisibility definition of probable prime and the modeq definition. The hypothesis h is needed to deal with edge cases in the original definition

lemma probable_prime_iff_modeq (n : ℕ) {b : ℕ} (h : b ≥ 1) : probable_prime n b ↔ b^(n - 1) ≡ 1 [MOD n]

[Kevin Buzzard]

ab_lem is horrible because it's using natural subtraction. Do you really need that non-mathematical statement? It would be more natural to have a and b integers there.

[Kevin Buzzard]

You shouldn't have any lemmas with > in. You should change all a > b to b < a because that's the shape of all the hypotheses, conclusions, simp lemmas etc in all the lemmas in Lean's library

[Niels Voss]

I replaced all instances of > and ≥ with < and ≤ (with the exception of a few calc proofs where changing the symbol would have required changing the direction of proof).

I agree that ab_lem, in its current state, is a bit questionable because it relies on the fact that a - b = 0 when b > a. Is natural number subtraction bad in general, or just in cases where it leads to problematic results? I could add a ≥ b as a hypothesis. I could also make ab_lem use integers, and then use exact_mod_cast and similar tactics to use it to prove properties of natural numbers.

I think the problem is a bit deeper, though. The main reason why ab_lem needs to operate on natural numbers rather than integers is because my original definition used natural numbers instead of integers. I could change this (which would probably remove quite a few sore spots where linarith didn't solve inequalities as well as I would have hoped). However, I'm not quite sure how I would do this, since a^b is not defined when a and b are both ints. In the main definition

def fermat_psp.probable_prime (n : ℕ) (b : ℕ) : Prop := n ∣ b^(n - 1) - 1

n - 1 needs to be a nat because it is the exponent. I could maybe try one of these:

def probable_prime (n : ℕ) (b : ℤ) : Prop := ↑n ∣ b^(n - 1) - 1
def probable_prime (n : ℕ) (b : ℤ) : Prop := 1 ≤ n ∧ ↑n ∣ b^(n - 1) - 1
def probable_prime (n : ℕ) (b : ℕ) : Prop := 1 ≤ n ∧ ↑n ∣ (b : ℤ)^(n - 1) - 1

and see how far I get.

[Kevin Buzzard]

Natural number subtraction is a pathological function so it's harder to work with. The books you were taking the proofs from didn't use it, right? Mathematicians don't use it, right? So why use it here?

[Kevin Buzzard]

I'm not suggesting you change the power to an integer though! That would also be pathological because what would the integer 2^-1 be? All I'm saying is that rather than fight natural subtraction like the computer scientists do, avoid it like the mathematicians do.

[Niels Voss]

Yes, I think you're right. Upon looking over my proof again, the only natural number subtraction that I ended up performing was something minus one. My proof is based roughly on this one: https://primes.utm.edu/notes/proofs/a_pseudoprimes.html

The only natural number subtraction in this proof I used often was subtracting 1 from various numbers, the idea being that none of the numbers that 1 was subtracted from are ever going to be 0. I just realized in my proof that whenever I use ab_lem, I set b to be 1 as well, so I could probably do with a more restricted form of ab_lem:

lemma ab_lem' (a n : ℕ) : (a - 1) ∣ (a^n - 1)

I'm not really sure why I decided to generalize it to all b, I just assumed that I might need it at one point. Is natural number subtraction with 1 still a problem if the only times it would be irregular is during edge cases?

I used natural number subtraction with numbers other than 1 twice, but only to prove a very specific subgoal and not in a definition or theorem statement so it probably isn't worth considering.

[Kevin Buzzard]

I'm just saying that in my experience, avoiding natural subtraction completely makes proofs easier. If you've already done what you need to do using it, that's fine -- it's more advice than anything else, and there are more CS-aligned people around here who would probably disagree with it.