Primitive Sets Above x in Lean

This repository formalizes a solution to Erdős Problem #1196, which asks whether every primitive set supported on [x, ∞) satisfies

$$\sum_{a \in A} \frac{1}{a \log a} \le 1 + o(1) \qquad (x \to \infty).$$

The formalized result proves the quantitative estimate

$$\sum_{a \in A} \frac{1}{a \log a} \le 1 + O\!\left(\frac{1}{\log x}\right) \qquad (x \to \infty),$$

for every primitive set A ⊆ ℕ ∩ [x, ∞). The argument follows the explicit sub-Markov-chain construction in source.tex, where the visiting probabilities are proportional to 1 / (n log n).

Highlights

• PrimitiveSetsAboveX.mainTheorem in PrimitiveSetsAboveX/Main.lean formalizes the main bound for Erdős Problem #1196.
• Erdos1196.erdos_1196 in PrimitiveSetsAboveX/FormalConjecturesErdos1196.lean packages the result in the same mathematical form as the formal-conjectures statement of Erdős Problem #1196.
• The repository includes the Lean development, a blueprint, and the TeX source for the writeup.

Repository Structure

• PrimitiveSetsAboveX/Basic.lean and PrimitiveSetsAboveX/PrimitiveWeight.lean define primitive sets, weights, and the weighted series.
• PrimitiveSetsAboveX/Preliminaries.lean, PrimitiveSetsAboveX/NormalizationCore.lean, and PrimitiveSetsAboveX/NormalizationSmallPrime.lean establish the analytic normalization estimates.
• PrimitiveSetsAboveX/Markov.lean develops the sub-Markov chain and its explicit visit formula.
• PrimitiveSetsAboveX/HitMass.lean implement the first-hit mass argument leading to the final weighted-series bound.
• PrimitiveSetsAboveX/Main.lean assembles the full theorem.
• PrimitiveSetsAboveX/FormalConjecturesErdos1196.lean provides a bridge theorem matching the formal-conjectures statement for Erdős Problem #1196.
• blueprint/src/content.tex and blueprint/src/sections/ contain the blueprint source.
• source.tex contains the TeX source for the accompanying writeup.

Key Links

• Erdős Problem #1196
• Main theorem in Lean
• Formal-conjectures style theorem in Lean
• TeX writeup source
• Blueprint source

Useful Commands

Compile the Lean development:

lake exe cache get && lake build

Build the blueprint PDF:

uvx leanblueprint pdf

Build and serve the blueprint website:

uvx leanblueprint web && uvx leanblueprint serve

Build the TeX writeup PDF:

latexmk -pdf source.tex