How to write about there are infinite primes p % 4 = 3

Stream: new members

[Elizabeth Sun]

Hi, I'm think about how to write about there are infinite primes that are congruent to 3 mod 4.

[Johan Commelin]

One way would be:

example : \forall n, \exists p, p ≥ n \and p.prime \and p % 4 = 3 := sorry

[Yury G. Kudryashov]

Did you ask how to formalize the statement, or which proof is simple enough to be formalized?

[Elizabeth Sun]

I mean the statement

[Elizabeth Sun]

Okay, thank you but I think we should say \exists p : nat, right?

[Yury G. Kudryashov]

You can write exists p >= n, p.prime, and lean will figure out the type.

[Elizabeth Sun]

trial2:10:28: error
don't know how to synthesize placeholder
context:
⊢ Sort ?
trial2:10:39: error
invalid expression starting at 10:31
trial2:10:42: error
unknown identifier 'p.prime'
trial2:10:53: error
unknown identifier 'p'

No, mine shows the errors.

[Johan Commelin]

Do you have import data.nat.prime?

[Elizabeth Sun]

emmmm...no....

[Elizabeth Sun]

but there is still the error

[Johan Commelin]

Did you take my statement or Yury's?

[Elizabeth Sun]

I took yours and Yury's, but neither worked unless I added p:nat

[Johan Commelin]

Ok, too bad

[Yury G. Kudryashov]

Indeed, you have to specify the type at least once

[Yury G. Kudryashov]

For n or for p

[Yury G. Kudryashov]

Or use nat.prime p instead of p.prime

[Yury G. Kudryashov]

Sorry for a misleading comment

[Elizabeth Sun]

Oh, it's okay, thank you!

[Kevin Buzzard]

As for the proof, if you have finitely many primes congruent to 3 mod 4 then multiply them all together, square, and add two, and then one of the factors must be a new prime congruent to 3 mod 4.