Number theory

Dickson

**Dickson's conjecture** If a finite set of linear integer forms

f_i(n) = a_i n+b_i

satisfies Schinzel condition, there exist infinitely many natural numbers

m

such that

f_i(m)

are primes for all

i

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.Wikipedia.Dickson
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Dickson.dickson_conjecture" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∀ (fs : Finset (Polynomial ℤ)),
  (∀ f ∈ fs, f.degree = 1 ∧ BunyakovskyCondition f) →
    SchinzelCondition fs → Infinite ↑{n | ∀ f ∈ fs, Nat.Prime (Polynomial.eval (↑n) f).natAbs}

Original conjecture source: FormalConjectures/Wikipedia/Dickson.lean

Source type SHA-256: sha256:1ebd92800eb4ec222607e75a5faffe877b94086637852630bf25b120af28eeff
Task id: fc-v2-dickson-dickson-conjecture-6be74425bfefc7e270f2148f-formalized
Task commitment: sha256:fe9bc650d6858a7d9d882038330719e30b89df5041bef95eebb58f11917452bd

References

Leonard Eugene Dickson, History of the Theory of Numbers, Vol. I: Divisibility and Primality

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

∀ (fs : Finset (Polynomial ℤ)), (∀ f ∈ fs, f.degree = 1 ∧ BunyakovskyCondition f) → SchinzelCondition fs → Infinite ↑{n | ∀ f ∈ fs, Nat.Prime (Polynomial.eval (↑n) f).natAbs}