Number theory

Hardy Littlewood - first hardy littlewood conjecture

Let

P = (m_1, \dots, m_k)

be a tuple of distinct positive even integers. Let

\pi_P(n)

denote the number of primes

p\leq n

such that

(p, p + m_1, \dots, p + m_k)

forms an admissible prime constellation. Let

w(q; m_1, \dots, m_k)

denote the number of distinct residues of

0, m_1, \dots, m_k

modulo

q

, and let

C_P = 2 ^ k\prod_{\substack{q\ \text{prime} \\ q\geq 3}} \frac{1 - \frac{w(q; m_1, \dots, m_k)}{q}}{\left(1 - \frac{1}{q}\right)^{k+1}}.

Then

\pi_P(n)\sim C_P\int_2^n\frac{dt}{\log^{k+1}t}.

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.HardyLittlewood
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "HardyLittlewood.first_hardy_littlewood_conjecture" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∀ {k : ℕ} (m : Fin k.succ → ℕ), HardyLittlewood.FirstHardyLittlewoodConjectureFor m

Original conjecture source: FormalConjectures/Wikipedia/HardyLittlewood.lean

Source type SHA-256: sha256:115d3ca4efee8567e3fd85b1b525c3a55dfc0282397397bf3b4872ff2d4d1f25
Task id: fc-v2-hardylittlewood-first-hardy-littlewood-conjecture-865ad81b96b4a43b043d6031-formalized
Task commitment: sha256:6667e2e5213dea32d0f9d6a6ade19c397d6495b3cd3f8de0f38c7c6cddb21014

References

Wikipedia

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