Formal target: Corpus.WikipediaHardyLittlewood.first_hardy_littlewood_conjecture

Let $P = (m_1, \dots, m_k)$ be a tuple of positive even integers.

Exact formal statement

∀ {k : Nat} (m : Fin k.succ → Nat), Corpus.WikipediaHardyLittlewood.FirstHardyLittlewoodConjectureFor m

This target is a formal statement, not a proof of the problem.

Environment availability: available.