folklore/"joke" theorem

Stream: Is there code for X?

[Alex Kontorovich]

I was discussing this "joke" theorem with some students (about the dangers of ineffective implied constants, which are all over some big parts of analytic number theory...), and they asked if it could be formalized in Lean. I said, of course, and it took two minutes to do so. I'm assuming this isn't the kind of thing that people would want in mathlib, right?

import data.int.basic
import tactic

/-- A natural number `n` is a `twin_prime` if it and `n+2` are both `prime`. -/
def twin_prime (n : ℕ) : Prop := prime n ∧ prime (n+2)

/-- The Twin Prime Conjecture states that there are infinitely many twin primes.
  Equivalently, for any `C`, there exists `n>C` which is a `twin_prime`. -/
def twin_prime_conj : Prop := ∀ C, ∃ n > C, twin_prime n

/-- The Iwaniec/Heath-Brown (folklore/joke) Theorem states that there is a constant `C` so that:
  If you can find a `twin_prime` greater than `C`, then there are infinitely many such. -/
theorem twin_primes_C : ∃ C, (∃ n > C, twin_prime n) → twin_prime_conj :=
begin
  by_cases H : twin_prime_conj,
  { refine ⟨1, λ x, H⟩, },
  { dsimp [twin_prime_conj] at H,
    push_neg at H,
    obtain ⟨C, hC⟩ := H,
    use C+1,
    intros hh,
    exfalso,
    obtain ⟨n, HH, hn⟩ := hh,
    have : C < n := by linarith,
    exact hC n this hn, },
end

[Scott Morrison]

If we don't put things like this into mathlib (ideally with a doc-string clearly explaining the joke), how are our new AI overlords ever going to gain a sense of humour?

[Alex Kontorovich]

Right. Except that, if/when we get around to formalizing the Deuring/Heilbronn phenomenon, we'll be making a similar kind of "joke", but in that case, it will be solving the Gauss class number problem... So...?

[Junyan Xu]

I think it's an specialization of https://en.wikipedia.org/wiki/Drinker_paradox

[Junyan Xu]

https://www.codewars.com/kata/5e3cd88fa5b6a8001fa84ed5/train/lean

[Alex Kontorovich]

That's a fun re-statement. I'm guessing that the "Drinker" version (from the 70's?) is a reformulation of something like Deuring-Heilbronn (from the 30's), which I believe is the first time such an argument appeared in serious mathematics... (But I'm not an historian...)

[Matt Diamond]

@Alex Kontorovich on a side note, if you just use C in your proof instead of use C+1 then you don't need to use linarith

[Alex Kontorovich]

Yes, of course. But (analytic) number theorists have to put the +1. You know, just in case... :joy: