Introduction

This is an interactive blueprint to help with the formalisation of the main result of (https://arxiv.org/abs/2112.03726): that if \(A\subset \mathbb {N}\) has positive density then there are distinct \(n_1,\ldots ,n_k\in A\) such that \(\frac{1}{n_1}+\cdots +\frac{1}{n_k}=1\).

(And other more precise results formulated in that paper.) For context, background, references, and so on, we refer to the original paper (https://arxiv.org/abs/2112.03726). This blueprint will (once finished) be a complete mathematical guide to the entire proof, and indeed the proofs will be in many places expanded and explained more fully, to help the formalisation process.

Nonetheless, we will be sparing with non-mathematical remarks, and will not usually trouble to explain the context of a particular lemma, or what it’s ‘really saying’, and so on – we will present everything necessary to formalise the proof in Lean, no more and no less.

The actual Lean code can be found at (https://github.com/leanprover-community/mathlib/blob/unit-fractions/src/number_theory/unit_fractions.lean). If you’d like to contribute in any way, or have any questions about this project, please email me at bloom@maths.ox.ac.uk.

This blueprint is adapted from the blueprint created by Patrick Massot for the Sphere Eversion project (https://github.com/leanprover-community/sphere-eversion).

This blueprint uses Patrick Massot’s leanblueprint plugin (https://github.com/PatrickMassot/leanblueprint) for plasTeX (http://plastex.github.io/plastex/).