All missions

Packing equal balls in three dimensions

The Kepler conjecture asks how much of three-dimensional Euclidean space can be filled by congruent solid balls whose interiors do not overlap. It is a question about all arrangements, including irregular arrangements with no repeating cell. A lattice calculation can exhibit an efficient packing but cannot bound every packing. The result is a central extremal theorem of discrete geometry and a substantial example of a proof combining geometry with finite computation. Hales published a proof in 2005; the later Flyspeck project verified a revised proof in HOL Light and Isabelle. This mission concerns a Lean 4 formalization of that verified result. Its authority is Hales et al., A Formal Proof of the Kepler Conjecture (2017), especially sections 3–4.

Centers, separation, and finite containers

A unit-sphere packing is a set $V\subseteq\mathbb R^3$ of centers such that $\|u-v\|\ge2$ whenever $u,v\in V$ are distinct. The occupied region is the union of the open balls $B(v,1)$. Tangency is allowed. The ambient metric is the Euclidean metric, represented by EuclideanSpace ℝ (Fin 3).

For a real radius $r$, write $N_V(r)=\#(V\cap B(0,r))$, where the observation ball is open. Uniform separation makes this intersection finite. The definition of a packing does not assume that the whole set is finite, periodic, saturated, or contains the origin. A saturated packing is one to which no further center can be added while preserving separation. Saturation occurs in an intermediate theorem; an extension theorem must remove it before the final conclusion. These conventions follow the formal source statement and the packing definitions in the accompanying repository.

Formalization targets

The source-faithful goal is

The constant may depend on the packing and must work for every indicated radius. This is the finite-container statement displayed in Hales et al., section 3, published PDF page 6. Its quadratic boundary term is part of the target.

Two additional statements record the conventional density consequence. Define the upper packing density by

The optional targets are $\overline\delta(V)\le\pi/\sqrt{18}$ for every packing and $\sup_V\overline\delta(V)=\pi/\sqrt{18}$. They are separate from the core theorem. The analytic count-to-volume bridge and the explicit face-centered cubic witness $\sqrt2\{z\in\mathbb Z^3:\sum_i z_i\equiv0\pmod2\}$ are stated independently. The density need not have an actual limit. This distinction also makes comparison with the current Lean-Eval statement precise.

What the formalization contributes

The finite-container theorem bounds every arrangement at every radius at least one, up to its stated boundary error. The density corollary identifies the optimal asymptotic occupied fraction once a close-packing witness is supplied. It makes no uniqueness assertion: an upper bound and an attaining example do not classify all optimizers. The normalizing unit-ball volume is $4\pi/3$; it cancels against the same factor in the observation-ball volume when comparing $N_V(r)/r^3$ to occupied density. The Blueprint, section 1.2, describes the close packings.

Flyspeck already provides a machine-checked proof in its original systems. The work here is to express and prove the same mathematics with Lean's kernel and Mathlib, and to develop reusable geometric, combinatorial, and certificate interfaces. Existing partial Lean 4 work is acknowledged; no priority claim is made. The proposal supplies statements and conditional assembly, not a completed Lean proof.

Why the interfaces matter

The revised proof does not reduce to optimizing a lattice cell. Its local configurations have varying combinatorial types, and the necessary nonlinear estimates and linear relaxations must apply to all their geometric realizations. The primary account, sections 4–9, distinguishes the geometric argument, nonlinear inequalities, tame-graph classification, and linear-program verification. The public milestones preserve these distinctions and use the revised annulus estimate, rather than importing the original decomposition-star architecture unchanged.

Formalization scope and verification

Seven milestones cover packing foundations; the fixed nonlinear catalog; the global geometric reduction; extraction and tameness of a local counterexample; archive classification; exhaustive geometric LP certificates; and the local annulus bound. The last states that every finite packing in $2\le\|v\|\le2.52$ satisfies $\sum_v(2.52-\|v\|)/0.52\le12$. This is section 4.2, equation (1). A compiled conditional theorem composes these interfaces into the exact final goal.

The nonlinear catalog contains actual real formulas from the six selectors in the pinned final Flyspeck statement: 580 family occurrences indexing 539 distinct source-ID records. These 539 source IDs have 498 distinct normalized syntactic bodies; repeated formulas are retained, and no claim of semantic inequivalence is made. All 539 domains have separately kernel-checked witnesses; this does not prove the inequalities. The graph archive is fixed independently of tameness. The reported 18,762 matches the AFP 2013-12-11 archive: 9 triangular, 1,105 quadrilateral, 15,991 pentagonal and 1,657 hexagonal cases. The AFP entry records a change of tameness constants and archive on 3 July 2014. The final archive has 19,715 rows: 9 + 1,253 + 16,080 + 2,373; the pinned make_archive.hl explicitly records this July-2014 count. Exact permutation comparison shows all 18,762 older classes retained and 953 added, with no duplicate or mirror-equivalent rows within either archive. The mission uses the final accompanying archive, whose source SHA-256 is 703ea865a124aa69f0ee12d94df7065bbbf5701a3085776e24632d14493474db. These are candidate graphs: the classification is coverage, not a claim that every stored row is tame or geometrically realizable (primary §7.2).

The final LP family is pinned to the completed Flyspeck revision 1ce0353008eba83d3c76ae9a25c3c242e4802d53: 19,715 graph-indexed trees and exactly 43,078 leaves from all 39 final binary containers. Every branch, face refinement, rounded row template and selected row index is concrete Lean data. The 42,889 objective-bound leaves include the source score-lower-bound row; 189 leaves are direct infeasibility cases. M6 requires complete decoding, local feasibility at the fixed geometric evaluator, and a checked rational certificate for every structural leaf, including unreachable leaves. Solvers cannot replace the source family by a freely chosen LP. See the completed source verifier and primary §9.

The fixed LP selector table is split into forty consecutive data definition files. The archive and graph case trees each occupy two data files, with separate reusable interfaces. Every definition file is below 900,000 UTF-8 bytes, within the platform's observed 1,048,576-byte scanner limit. Ordered concatenation preserves all 19,715 archive records, 19,715 graph trees and 43,078 LP leaves; this packaging adds no mathematical assumption or milestone.

External search may generate data. Coverage, real-expression bounds, exhaustive branching, and rational infeasibility must be justified by Lean theorems. Interval/Taylor certificates have separate encoding, acceptance, and soundness obligations; exact rational LP soundness and the conditional assembly are already checked infrastructure. Floating-point optimization, source hashes, and unchecked native computation are not proofs. All statements target Lean 4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f.

Selected references

• Hales et al., A Formal Proof of the Kepler Conjecture, Forum of Mathematics, Pi 5 (2017), e2. DOI, arXiv.
• Hales, Dense Sphere Packings: A Blueprint for Formal Proofs, Cambridge University Press (2012). Author's extended version.
• Hales, A Proof of the Kepler Conjecture, Annals of Mathematics 162 (2005). Paper.
• Bauer and Nipkow, Flyspeck I: Tame Graphs. Archive of Formal Proofs.
• Solovyev and Hales, Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations (2013). Paper.
• Solovyev and Hales, Efficient Formal Verification of Bounds of Linear Programs. Paper, sections 2–3.

Why formalize the Four Color Theorem in Lean 4?

The Four Color Theorem links a short mathematical statement to a large collection of finite checks. For contributors to graph theory and proof assistants, it is a concrete test of whether abstract mathematics, executable verification, and a public theorem statement can share one auditable foundation. The proposed result is a complete Lean 4 formalization, reusing Mathlib and adapting the established proof architecture to Lean.

The mathematical result is established. Robertson, Sanders, Seymour, and Thomas gave a modern computer-assisted proof in 1997. Gonthier subsequently developed a Coq formalization covering both mathematical reasoning and computation, described in his 2005 report and 2008 Notices article. This mission is classified as ResearchPaper because it formalizes these published results. (RSST, Gonthier 2005, Gonthier 2008)

Graphs, drawings, and colors

The root Lean interface uses Mathlib's SimpleGraph: a finite vertex set with a symmetric, irreflexive adjacency relation. Edges in this representation carry no additional identities or multiplicities. The conventional statement also permits parallel edges. Already-proved local infrastructure uses Mathlib's Graph V E to erase parallel edges while preserving a genuine plane drawing and proper vertex colorings; only the actual vertex set must be finite. A proper vertex coloring assigns a color to every vertex and assigns different colors to adjacent vertices. Four available colors means at most four colors are used; there is no requirement that each color occur.

A planar drawing places distinct vertices at distinct points of the real plane and represents each edge by an injective continuous arc joining its endpoints. An arc contains no other vertex, and arcs of different undirected edges meet only at shared endpoints. Reversing the orientation of an edge reverses its parameterization. A graph is planar when such a drawing exists. This is a geometric condition independent of coloring and of the eventual configuration checkers. Gonthier discusses the graph-embedding formulation in Section 2, PDF p. 4 of the 2005 report.

Write $V$ for the vertex set, $G$ for its adjacency relation, and $C=\{0,1,2,3\}$ for the available colors. Empty graphs, isolated vertices, and disconnected graphs are included. The drawing is a witness to a hypothesis; the theorem does not impose coordinates, a prescribed embedding, or a straight-line representation.

Formalization target

For every finite loopless planar graph, establish

The draft Lean target is FourColor.four_color: for every finite vertex type and every SimpleGraph on that type, FourColor.IsPlanar G implies G.Colorable 4. Its graph formulation follows RSST's Section 1, PDF p. 2 of the author-hosted manuscript. The manuscript's PDF page numbers differ from the journal's pagination.

The exact unchanged root signature is:

FourColor.four_color.{u} :
  ∀ (V : Type u) [Finite V] (G : SimpleGraph V),
    FourColor.IsPlanar G → G.Colorable 4

This is an open target signature, not a completed proof. The existing FourColor.FinalAudit.multigraph_four_color_of_necessary_targets conditionally connects the mission obligations to the conventional finite loopless planar multigraph statement. Its drawing has distinct vertex positions and injective continuous arcs for each edge identity; erasing parallel edges is proved to preserve planarity and every proper-coloring constraint. This bridge adds no simplicity, connectedness, triangulation, or nonemptiness assumption to the conventional conclusion. The root target itself remains unchanged.

An equivalent combinatorial formulation is welcome only with the formally verified translations needed to recover this target. If equivalence is claimed, both directions must be proved under precisely stated conventions. In particular, a hypermap coloring theorem alone does not complete this mission.

The original seven structural milestones remain unchanged:

These correspond to Gonthier's reductions in Section 3, PDF pp. 6–9, and development in Sections 5.1–5.6 of the 2005 report. Exact locations and executable-reference declarations accompany each milestone. Milestones 2, 3 and 6 imply milestone 7; milestones 1 and 7 imply the graph target. Those two conditional implications have been checked in Lean against the exact proposed statements. Milestone 6 now has thirteen concrete supporting targets:

The fixed catalogue and fixed rules are shared by both branches. The local Lean assembly checks that reducibility, geometric exclusion, reflection, the transfer bound, the seven degree cases, and milestones 4–5 imply milestone 6. It then connects to the unchanged hypermap and graph targets. The generic presentation checker offers a sufficient route to the semantic degree targets; its ability to certify every source presentation is not presumed. That route also requires actual presentation certificates and proofs of acceptance for the degree cases. Generic soundness and catalogue geometry alone do not supply those witnesses. Direct proofs of the seven semantic coverage obligations remain valid. Catalogue geometry remains a separate, meaningful finite theorem.

Exact mission obligations

There are 21 open theorem targets: 20 supporting milestones and one root. Every name below has prefix FourColor.. All remain future mission work; the checked conditional assembly is not a proof of any of these targets.

The degree cases quantify over minimal counterexamples with the exact positive score defined by the fixed rules; neighboring degrees have no artificial upper bound. The dependency path uses 16 necessary input targets to derive targets 19, 20 and 21. Targets 6 and 10 support the optional presentation-certificate route. None of targets 19, 20 or 21 is assumed as a shortcut in this assembly.

What completion would provide

The theorem provides a uniform existence guarantee for all finite planar graphs, without a bound on their size. Its Lean development should also make reusable graph embeddings, finite combinatorial maps, coloring transports, and verified finite checkers available to later work.

The existing Rocq development is an executable reference for definitions, dependency structure, and proof behavior. It is not a proof import into Lean. The proposed contribution is a Lean development whose proof objects and computation are justified within Lean's documented foundations. A mechanically translated collection of scripts is not required; contributors should choose abstractions that work well with Mathlib.

Where the difficulty lies

Checking finitely many small graphs does not establish the theorem for arbitrary finite graphs. The development must justify why its finite computational tasks suffice, and must connect their results to the graph statement. The mathematical and computational obligations must meet at explicit, proved interfaces.

There is also a representation gap. The standard target concerns vertex colorings of graphs drawn in the plane, whereas the reference implementation's combinatorial core colors faces of planar bridgeless hypermaps. The latter endpoint is four_color_hypermap in combinatorial4ct.v. Correct treatment of duality, connected components, and isolated vertices is part of the work. Renaming a combinatorial predicate “planar” cannot establish that connection.

Formalization scope and acceptance criteria

Use Lean 4 with a supported, pinned Mathlib revision. The initial draft is checked against Lean v4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Any later migration must preserve the statements and repeat the relevant checks. Reuse Mathlib's graph and coloring interfaces where appropriate, and develop missing infrastructure as reusable modules. The topological definition must not assume colorability, successful certificate verification, or the conclusion of an intermediate theorem.

The definition layer now provides plane drawings, finite permutation hypermaps, an exact graph/face incidence representation, minimal counterexamples, and rational face charges. Coloring equivalence across a face representation is proved for every positive number of colors, with isolated vertices handled explicitly. Exact Euler equality defines combinatorial planarity; geometric realization is a theorem obligation and cannot be assumed from the name.

The concrete core now defines configurations, ordered boundary traces, contracts, chromograms, Kempe closure, kernel preembeddings and reflected occurrences. The reference reducibility checker has proved soundness and completeness. All 633 maps, rings and contracts are literal data with kernel-validated table/index proofs. The 38 base entries and their 71 symmetrized entries are explicit, and the executable matcher has proved semantic correctness. These infrastructure results do not prove the catalogue's geometric validity, its reducibility, or unavoidability.

The production targets import FourColor.CompactCatalogue.configurations, a compact catalogue containing the same literal maps, rings and contracts. A generic verified decoder constructs validated entries without storing large evaluated proof terms in every import. A separate kernel-checked comparison proves exact ordered equality with the original catalogue, proves that every raw entry is accepted, and proves that none is dropped. The original certificate batches remain available for that audit but are excluded from production target imports. This representation change does not alter any of the 21 mathematical obligations.

Data provenance is pinned to Rocq commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Independent fresh-source comparisons check all 633 configurations and every base/expanded rule entry against that snapshot, including actual evaluated Lean payloads. These comparisons establish source correspondence; they are not proofs of reducibility or unavoidability.

The duplicate-data gate rejects unexplained or unintended duplicates and permits verified source-mandated repetition encoding multiplicity or weight. The only repeated rule payload is drule1, deliberately listed twice: the source explains its two-point transfer in discharge.v, lines 17–24 and retains both copies in base_drules (line 145). The Lean rule-match count also counts both copies, preserving weight two. Thus there are 38 base entries with 37 distinct payloads, and 71 expanded entries with 70 distinct payloads. Both copies must remain. No configuration duplicates or other repeated rule payloads are permitted without separately verified source justification.

The reference reducibility evaluator is exponentially expensive. Contributors should implement verified compressed representations or efficient checkers, with acceptance implying the same semantic C-reducibility. Completeness of the reference checker then recovers the stated certificate-existence target. The presentation language is a transparent finite baseline; its generic soundness is an open target, and no completeness claim is made. Source-style quizzes/hubcaps or direct Lean proofs can close the same seven semantic coverage targets. This keeps performance choices separate from the mathematical endpoint.

All computational claims needed by the theorem must be established in Lean. External generators may prepare candidate data or certificates, but their output must be validated by a checker with proved correctness, and the resulting proof must be accepted by the Lean kernel. A recorded successful run of an external program is insufficient. The final theorem and its dependency closure must contain no sorry, admit, unproved custom axiom, or unsupported computational assumption. An axiom audit must identify only Lean/Mathlib's documented foundations. The current 37-declaration conditional/infrastructure audit uses only propext, Classical.choice and Quot.sound; it does not claim an unconditional Four Color proof. Python generators and runtime JSON extraction are outside the mathematical trust boundary and cannot discharge the 21 targets.

Completion requires a reproducible repository in which lake build succeeds from a clean environment and builds the final theorem. Pin toolchain, dependencies, source revisions, and certificate data; document regeneration and verification commands. Maintain a dependency map connecting Lean declarations to exact paper locations and Rocq declarations, and record justified differences in representation. The local multigraph adapter already justifies forgetting parallel-edge multiplicities and transports proper colorings. Any auxiliary restrictions such as connectedness or nonemptiness must be discharged before the root theorem. The current statement and conditional builds verify proposal infrastructure. Success requires proofs of the mission obligations and the final theorem in the reproducible clean build, with no unproved assumptions beyond the documented Lean/Mathlib foundations. All 21 targets remain open at proposal finalization. The submission snapshot records the repository base commit, exact working-file hashes, toolchain, Mathlib revision, payload hashes and audit report; it must not misrepresent uncommitted files as contents of the base commit.

Selected references

• Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem, technical report, 2005. Sections 2–5. Microsoft Research PDF.
• Georges Gonthier, Formal Proof—The Four-Color Theorem, Notices of the AMS 55(11), 1382–1393, 2008. Theorem 1 and the formalization architecture. AMS PDF.
• Gonthier and Rocq-community contributors, fourcolor, executable formalization, pinned to commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Repository.
• Neil Robertson, Daniel Sanders, Paul Seymour, Robin Thomas, The Four-Colour Theorem, Journal of Combinatorial Theory, Series B 70(1), 2–44, 1997. DOI; author-hosted manuscript.

Motivation

The Collatz map sends an even positive integer $n$ to $n/2$ and an odd one to $3n+1$. The Collatz conjecture asserts that every orbit of this map eventually reaches $1$. It remains an open problem.

Because the conjecture is open, a large part of the literature proves weaker statements that hold for almost all starting values. These results bound how small an orbit gets, not whether it reaches $1$. They are the strongest unconditional evidence for the conjecture. Terence Tao's 2022 theorem is the strongest result of this type: outside a set of logarithmic density zero, every orbit drops below any prescribed function that tends to infinity, however slowly (Tao 2022).

Timeline

Attributions follow the survey in Tao 2022, Section 1. Here $\mathrm{Col}_{\min}(N)$ is the least value in the orbit of $N$.

• 1976 to 1979, Terras and Everett. $\mathrm{Col}_{\min}(N) < N$ for almost all $N$, in natural density.
• 1979, Allouche. $\mathrm{Col}_{\min}(N) < N^{\theta}$ for almost all $N$, for every $\theta > 0.869$.
• 1994, Korec. The same bound for every $\theta > \log 3/\log 4 \approx 0.7924$.
• 2019 preprint, 2022 publication, Tao. The power $N^{\theta}$ is replaced by any $f(N) \to \infty$, in logarithmic density instead of natural density (Forum of Mathematics, Pi 10, e12).
• 2026, ProofAtlas. A complete machine-checked proof of Tao's theorem in Lean 4 is published (formalization record).

Setting

Let $\mathrm{collatzStep} : \mathbb{N} \to \mathbb{N}$ be

Write $\mathrm{collatzStep}^{[k]}$ for the $k$-fold iterate, with $\mathrm{collatzStep}^{[0]}(n) = n$. The orbit of $n$ is the set of values $\mathrm{collatzStep}^{[k]}(n)$ for $k \ge 0$. It includes $n$ itself.

The Syracuse map acts on odd integers. It sends an odd $n$ to the odd part of $3n+1$, which is $\mathrm{syracuseStep}(n) = (3n+1)/2^{\nu_2(3n+1)}$. The Syracuse orbit minimum $\mathrm{syracuseOrbitMin}(n)$ is the least value $\mathrm{syracuseStep}^{[k]}(n)$ over $k \ge 0$.

For a set $A$ of positive integers and a real cutoff $x \ge 2$, the logarithmic mass of $A$ up to $x$ is

A set of positive integers has logarithmic density $d$ when this quantity tends to $d$ as $x \to \infty$. Since $\sum_{n \le x} 1/n = \log x + O(1)$, all positive integers together have logarithmic density $1$, and the odd positive integers have logarithmic density $1/2$.

A function $f : \mathbb{N} \to \mathbb{R}$ tends to infinity on positive inputs when for every real $M$ there is an $N$ such that $f(n) > M$ for all $n \ge N$ with $n > 0$.

Formalization targets

Goal: Tao's Theorem 1.3

For every $f$ that tends to infinity on positive inputs,

This is the Lean theorem collatz_almost_bounded_logarithmic. It fixes no rate and no constant, so later improvements do not invalidate it.

Syracuse form: Tao's Theorem 1.6

For every $f$ that tends to infinity on odd positive inputs, the odd $n$ whose Syracuse orbit contains a value below $f(n)$ have logarithmic density $1/2$, which is all of the odd integers. This is syracuse_almost_bounded_logarithmic.

Quantitative form: Tao's Theorem 3.1

There are constants $C, c > 0$ such that for all real $M \ge 2$ and $x \ge 2$,

This is syracuse_uniform_logarithmic_tail_bound. The three targets are listed from weakest to strongest. In Tao's paper, the goal and Theorem 1.6 both follow from Theorem 3.1.

Significance

The result. Theorem 1.3 improves the earlier almost-all bounds on Collatz orbit minima from a power of $N$ to any function that tends to infinity. For example, $\mathrm{Col}_{\min}(N) < \log\log\log\log N$ for almost all $N$. The theorem does not settle the conjecture. A single divergent orbit or nontrivial cycle is not excluded, because its predecessors form a set with bounded orbit minima.

The formalization. The theorem is proved, and a complete formalization already exists. The ProofAtlas record Tao's Almost-Bounded Collatz Orbits proves the statement taoAlmostBoundedColMin_checked with the same step map and an orbit that includes its starting value. That package has 397 first-party Lean files and about 124,000 source lines. ProofAtlas records a passing build with no sorry and the axiom profile propext, Classical.choice, Quot.sound. The source is released under the Apache-2.0 licence at commit d53c8de00056fb05999e44589f2399d7efa026e4, with copyright held by Advameg, Inc. It was built with Lean v4.30.0-rc2.

The remaining work for this mission is therefore a port, not new mathematics. The existing Lean development must be moved to Lean v4.33.1 and Mathlib 0df444a, and then connected to the goal statement above.

Difficulty

The mathematical difficulty is already resolved in the existing proof. The classical first-descent argument shows that a typical orbit drops below its starting value. Repeating that argument fails, because after one descent the new value is no longer distributed like a random integer of its size, and the error compounds at each repetition. That is why earlier results stop at a power bound $N^{\theta}$.

The difficulty of this mission is engineering. The port moves a development of about 124,000 lines forward across three minor Lean releases and the corresponding Mathlib changes. Lemma renames, deprecations, and changes in tactic behaviour must be repaired file by file without changing any statement.

Formalization scope

• Step map. collatzStep n = if Even n then n / 2 else 3 * n + 1, so $\mathrm{collatzStep}(0) = 0$. This is the same definition as in the ProofAtlas source.
• Orbit. The witness $k$ ranges over all natural numbers, including $k = 0$.
• Density. The goal uses weightedLogMassReal: a real cutoff $x$, the natural indices $0 \le n \le \lfloor x \rfloor$, weights $1/n$, and normalization by $\log x$. The ProofAtlas statement instead uses integer cutoffs and normalization by the harmonic sum $\sum_{n \le N} 1/n$. A short bridge between the two normalizations is part of the required work.
• Threshold. The hypothesis on $f$ constrains only positive inputs. The value $f(0)$ is irrelevant.
• Non-triviality. The case $k = 0$ alone covers only inputs with $n < f(n)$. For slowly growing $f$ this set is finite, so the goal is not satisfied by the starting value.

The goal is already reduced, through accepted proofs, to the single open statement syracuse_uniform_logarithmic_tail_bound. Two routes therefore close the mission. The first is to port the ProofAtlas development and prove the goal directly through the density bridge. The second is to prove Theorem 3.1 in its stated form. Contributions welcome include ported modules as reusable solutions, the density bridge, and a proof of Theorem 3.1. Every ported file must keep the Apache-2.0 notice and attribution to the ProofAtlas source.

Selected references

• Terence Tao, Almost all orbits of the Collatz map attain almost bounded values, Forum of Mathematics, Pi 10 (2022), e12. https://doi.org/10.1017/fmp.2022.8 and https://arxiv.org/abs/1909.03562
• ProofAtlas, Tao's Almost-Bounded Collatz Orbits, Lean 4 formalization, source commit d53c8de00056fb05999e44589f2399d7efa026e4, Apache-2.0, 2026. https://proofatlas.ai/formalizations/tao-almost-bounded-orbits/
• Jeffrey C. Lagarias (editor), The Ultimate Challenge: The 3x+1 Problem, American Mathematical Society, 2010. https://bookstore.ams.org/MBK/78

Motivation

How many pairs of points in an $n$-point planar set can be at distance one? Counting all pairs gives the trivial bound $\binom n2$, but Euclidean geometry imposes a much stronger restriction: there are at most $Cn^{4/3}$ unit-distance pairs, for an absolute constant $C$.

This mission concerns that upper bound alone.

Statement

For a finite set $P\subseteq\mathbb R^2$, let $u(P)$ be the number of unordered pairs of distinct points at Euclidean distance one:

Prove that there exists a constant $C>0$ such that

for every finite $P\subseteq\mathbb R^2$. The constant must be independent of $P$, and there are no general-position assumptions.

Proof idea

The supplied proof uses the crossing lemma. From the unit circles centred at the points of $P$, it constructs an auxiliary graph with $n=|P|$ vertices and $e$ edges satisfying

If $e<4n$, then $u(P)<5n$. Otherwise, the crossing lemma gives

so $e\le \sqrt[3]{200}\,n^{4/3}$. Together, these cases give the required bound.

The main work is in constructing the graph, controlling its crossings, and proving the crossing lemma. The final numerical deduction is short. The project includes a written proof alongside the Lean development.

Lean formulation and scope

The plane is represented by EuclideanSpace ℝ (Fin 2) and point sets by Finset. The definition of unitDist P counts ordered pairs of distinct points at distance one, then divides by two.

The target proposition is:

∃ C : ℝ, 0 < C ∧
  ∀ P : Finset (EuclideanSpace ℝ (Fin 2)),
    (unitDist P : ℝ) ≤
      C * (P.card : ℝ) ^ ((4 : ℝ) / 3)

This includes empty and singleton sets and uses real exponentiation.

The crossing-consequences project already contains a sorry-free proof of this theorem. The purpose of the mission is to make it available for publication and community verification on Prove2me. The crossing lemma and other supporting results are not separate mission targets. Neither an optimal constant nor a matching lower bound is required.

References

• J. Spencer, E. Szemerédi, and W. T. Trotter, Jr., “Unit distances in the Euclidean plane,” in B. Bollobás (ed.), Graph Theory and Combinatorics, Academic Press, 1984, pp. 293–303. Full text.
• wpegden/crossing-consequences, commit 8769d142033fce042f502bf2857afb6b1375b5c3. Project overview and build instructions.

Motivation

Vehicle routing problems ask for minimum-cost vehicle routes that deliver goods from a depot to a set of customers. In the split-delivery vehicle routing problem with time windows (SDVRPTW) a customer's demand may be served by several vehicles, and each customer must be visited inside a prescribed time window. Allowing split deliveries matters in practice: for the variant without time windows, Dror and Trudeau (1989) showed empirically that splitting can save substantially, and Archetti, Savelsbergh and Speranza (2006) proved the savings can reach 50%.

Exact methods for the SDVRPTW are branch-and-price algorithms, and they rely on structural properties of optimal solutions to prune the search. Desaulniers (Operations Research 58(1), 2010) collects these properties in §2 of his paper and uses the strongest one, Corollary 2, as a family of valid inequalities (constraint (7)) in his branch-and-price-and-cut method.

Timeline (as reported by Desaulniers 2010, §§1–2).

• 1989–1990. Dror and Trudeau prove, for the SDVRP without time windows and with the triangle inequality, that some optimal solution has no two routes sharing more than one split customer.
• 2006. Gendreau, Dejax, Feillet and Gueguen observe that the property holds with time windows, derive the arc-based Corollary 1, and remark that elementary routes suffice (Remark 1).
• 2010. Desaulniers strengthens Corollary 1 to pairs of reverse arcs (Corollary 2) and exploits it as cutting planes.

Setting

An instance has $n$ customers $\mathcal N$, a start depot $0$ and an end depot $n+1$ (the same location at the beginning and end of the planning horizon), and the following data: a vehicle capacity $Q > 0$; a demand $d_i > 0$ for each customer, which may exceed $Q$; a time window $[e_v, l_v]$ for each node, shared by the two depot copies; nonnegative travel times $t_{vw}$, which include the service time at $v$; and nonnegative costs $c_{vw}$. The arc set $\mathcal A$ contains the idle arc $(0, n+1)$ and every arc $(v, w)$, $v \ne w$, with $e_v + t_{vw} \le l_w$. The triangle inequality $t_{vx} \le t_{vw} + t_{wx}$, $c_{vx} \le c_{vw} + c_{wx}$ is assumed throughout.

A route is a walk $0 \to v_1 \to \dots \to v_m \to n+1$ along arcs of $\mathcal A$, customers possibly repeated, with service start times inside the time windows that respect travel times (waiting is allowed), and nonnegative quantities delivered at its visits whose total is at most $Q$. Its cost is the sum of its arc costs. A solution is a finite family of routes, one per vehicle, with no bound on their number; it is feasible if every customer $i$ receives in total at least $d_i$, and optimal if it is feasible and no feasible solution costs less. For customers $i, j$, let $x_{ij}$ be the number of times arc $(i, j)$ is traversed, summed over all routes of a solution, and let $\mathcal A(\mathcal N) = \mathcal A \cap (\mathcal N \times \mathcal N)$.

Formalization targets

All four statements assume the triangle inequality and that the instance has a feasible solution, and assert the existence of an optimal solution with a structural property.

Goal: Corollary 2 (p. 181)

The two arcs of a pair of reverse customer arcs are used at most once in total. This is the form constraint (7) of the paper gives to the corollary.

Milestones

1. Remark 1. Some optimal solution has only elementary routes: no route visits a customer twice.
2. Theorem 1. Some optimal solution has no two distinct routes with two customers in common.
3. Corollary 1. Some optimal solution has $x_{ij} \le 1$ for all $(i, j) \in \mathcal A(\mathcal N)$.

Significance

The result. Corollary 2 turns a property of optimal solutions into linear inequalities on arc-flow variables. Adding them to the arc-flow formulation cuts off fractional points of its linear relaxation while keeping an optimal integer solution, which is how Desaulniers uses them. Remark 1 justifies pricing only elementary routes in column generation. Theorem 1 is the combinatorial fact underneath both corollaries and is reused throughout the split-delivery literature.

Formalizing it. The four results are proved in the literature (Dror–Trudeau; Gendreau et al. 2006); Desaulniers states them without proof. No machine-checked version exists. This mission produces a reusable Lean model of the SDVRPTW (instances, arc sets, feasible routes with schedules and delivery patterns, solutions, optimality) and checked proofs of these properties, including the existence of an optimal solution, which the paper takes for granted.

Difficulty

The obvious argument is local: take an optimal solution that violates the property, shift quantities between two routes, remove a visit, and shortcut. Three points make this less routine than it sounds. First, the statements are existential: each exchange must keep the solution optimal and not reintroduce a violation already removed, so one needs a termination measure that decreases under every exchange (Corollary 2 needs elementarity and the Theorem 1 property simultaneously, not two separate optimal solutions). Second, removing a visit is feasible only because the arc set is defined by time windows: the shortcut arc $(v, w)$ must be shown to exist from the schedule and the triangle inequality on travel times, and the new schedule must be built explicitly. Third, the feasible set is infinite (real quantities, unbounded walks, unbounded number of vehicles), so the existence of an optimal solution is itself a statement to prove, not a hypothesis.

Formalization scope

Namespace SplitDeliveryVRPTW.Known. Nodes are the inductive type Node n (start, cust i for i : Fin n, finish). All quantities, times and costs are real. The arc set is exactly the set the paper defines (read as "if and only if"), with arcs into the start depot and out of the end depot excluded. The triangle inequality for $t$ is imposed on pairwise distinct nodes and for $c$ on triples of arcs, where the paper's data is defined. A route is a customer list (repetitions allowed) with a time function over path positions and a quantity function over visits. A solution is an indexed family Fin m → Route I, so identical routes may appear twice. Demand satisfaction uses $\ge$, as constraint (2) does. The per-vehicle bound $\min\{d_i, Q\}$ of constraint (14) is omitted because it changes neither the feasible route patterns nor the costs.

Explicit readings of imprecise phrases:

• "split customer", "in common" (Theorem 1) are undefined in the paper. A customer two distinct routes visit is split, and the routes have it in common. This visit-based reading is at least as strong as a delivery-based one.
• Corollary 2's wording "at most one arc in set $\mathcal A^*_{ij}$ appears at most once" is read through constraint (7): the total number of traversals of the arcs of $\mathcal A^*_{ij}$ is at most one. It is stated in the equivalent form free of the choice of $\mathcal A^*(\mathcal N)$.
• "there exists an optimal solution" is conditional on feasibility, which is the hypothesis added.

Ruled-out trivializations: routes are not restricted to elementary walks (that would make Remark 1 definitional), solutions are not sets (that would forbid duplicate routes), optimality compares against solutions with any number of routes and any visit pattern, "split" is never counted over visits by the same route, capacity and time windows are part of route feasibility, and deliveries occur only at visits.

Useful infrastructure, reusable beyond this mission: shortcut lemmas for feasible routes (removing a visit), exchange lemmas between two routes, and existence of an optimum for split-delivery routing. Contributions of any of these as separate lemmas are welcome.

Selected references

• G. Desaulniers, Branch-and-Price-and-Cut for the Split-Delivery Vehicle Routing Problem with Time Windows, Operations Research 58(1):179–192, 2010. https://doi.org/10.1287/opre.1090.0713
• M. Dror, P. Trudeau, Savings by split delivery routing, Transportation Science 23(2):141–145, 1989. https://doi.org/10.1287/trsc.23.2.141
• M. Dror, P. Trudeau, Split delivery routing, Naval Research Logistics 37(3):383–402, 1990. https://doi.org/10.1002/nav.3800370304
• M. Gendreau, P. Dejax, D. Feillet, C. Gueguen, Vehicle routing with time windows and split deliveries, Technical Report 2006-851, Laboratoire Informatique d'Avignon, 2006.
• C. Archetti, M. W. P. Savelsbergh, M. G. Speranza, Worst-case analysis for split delivery vehicle routing problems, Transportation Science 40(2):226–234, 2006. https://doi.org/10.1287/trsc.1050.0117

Motivation

Many production and computing systems run jobs on parallel machines that also draw on a shared, limited resource: tools, workers, memory, power. Adding such a resource to a scheduling problem can change its complexity entirely. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the three-field classification $\alpha\mid\beta\mid\gamma$ of Graham, Lawler, Lenstra and Rinnooy Kan by a resource field $res\lambda\sigma\rho$, and determined the complexity of every problem with unit-time jobs on identical or uniform machines under the makespan criterion. Their Fig. 2 separates the maximal polynomially solvable cases from the minimal NP-hard ones.

This mission formalizes the polynomial side. Two identical machines are easy under arbitrary resources (Theorem 1, due to Garey and Johnson, via maximum matching). Three identical machines with one resource are NP-hard in the strong sense (Theorem 4), and so are two uniform machines with unit resources (Theorem 3). What remains for uniform machines is settled by two algorithms: a sorting-and-shifting procedure for two uniform machines with one resource of arbitrary size (Theorem 5), and a bottleneck transportation problem for any number of uniform machines with one resource and 0–1 requirements (Theorem 6). The hardness results are the subject of the companion missions I and II.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Machine $M_i$ has speed $q_i>0$; every job has unit execution requirement, so it takes time $1/q_i$ on $M_i$. Identical machines ($P$) have $q_i=1$; uniform machines ($Q$) have arbitrary speeds. There are $l$ resources $R_h$ with positive integer sizes $s_h$, and job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. The field $res\lambda\sigma\rho$ records restrictions: $\lambda$ bounds the number of resources, $\sigma$ their sizes, $\rho$ the requirements, a dot meaning "part of the input". So $res1{\cdot}{\cdot}$ is one resource with arbitrary size and requirements, and $res1{\cdot}1$ is one resource with requirements in $\{0,1\}$.

A schedule gives every job a machine $\mu(j)$ and a start time $S_j\ge0$; the job is executed during $[S_j,C_j)$ with $C_j=S_j+1/q_{\mu(j)}$. It is feasible if jobs on the same machine do not overlap and, at every time $t$, the jobs executed at $t$ use at most $s_h$ of each resource $R_h$. The makespan is $C_{\max}=\max_j C_j$. No precedence constraints occur in this mission.

Formalization targets

Goal: Theorem 5, correctness of the algorithm

For $Q2\mid res1{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ with $q_1\ge q_2$: put all jobs on $M_1$ in order of nonincreasing $r_{1j}$, then repeatedly move the last job of $M_1$ to the earliest feasible time on $M_2$ after the jobs already there, as long as this strictly reduces $C_{\max}$. For every order with nonincreasing requirements, the resulting schedule $A$ is feasible and

Milestones for the goal

The paper's proof has two steps, both milestones. Call a schedule an (a)–(c) schedule when (a) $M_1$ runs its jobs back to back from time $0$ in nonincreasing $r_{1j}$, (b) $M_2$ runs its jobs in nondecreasing $r_{1k}$, and (c) every requirement on $M_1$ is at least every requirement on $M_2$.

1. The algorithm's schedule is feasible, is an (a)–(c) schedule, and is best among feasible (a)–(c) schedules.
2. Every feasible schedule can be transformed into a feasible (a)–(c) schedule with no larger $C_{\max}$.

Further results

• Theorem 1. For $P2\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$, with $G$ the graph joining two jobs when they can run together and $S$ a maximum matching of $G$, the optimal makespan is $n-|S|$.
• Theorem 6. For $Q\mid res1{\cdot}1,\,p_j=1\mid C_{\max}$ with the $s_1$ fastest machines listed first, the optimal makespan equals the optimal value of a bottleneck transportation problem that assigns jobs to slots (machine, position) with cost $k/q_i$, resource jobs only to the $s_1$ fastest machines.

Significance

Theorems 5 and 6 complete the classification of Fig. 2 for uniform machines: every special case of $Q\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ not covered by the hardness theorems has a polynomial algorithm. Theorem 1 is the classical reduction of two-machine resource scheduling to maximum matching, the model case for later work on scheduling with conflict graphs.

The paper proves these results briefly: "clearly" for the first half of Theorem 5, "obviously" for Theorem 1, and a one-paragraph model for Theorem 6. The exchange argument of Theorem 5 is presented "in an informal way" through five steps that pass through fractional, preempted jobs. A machine-checked proof makes these arguments exact on a model with real start times. No formalization of these results is known, and the platform had no statement about resource-constrained scheduling on uniform machines before this mission.

Difficulty

With $q_1\ne q_2$ the job boundaries on the two machines are misaligned: a job on $M_2$ overlaps parts of several jobs on $M_1$, so the resource check cannot be done slot by slot, and discrete reasoning on integer time grids does not apply. The exchange argument of Theorem 5 must control the resource usage at every real time while jobs are moved between machines and reordered, and it has to end with a nonpreemptive schedule even though the paper's intermediate steps split jobs. For Theorem 1, the hard direction is the lower bound: a feasible schedule with arbitrary real start times must be converted into a matching, which is a statement about how unit jobs on two machines can overlap. For Theorem 6, one must show that restricting resource jobs to the fastest machines and to back-to-back positions loses nothing.

Formalization scope

• Model. Jobs, machines and resources are Fin n, Fin m, Fin l (0-based). Speeds are positive reals, sizes positive naturals, requirements naturals. Start times are nonnegative reals, execution intervals are half-open, and the resource constraint is checked at every real time. $C_{\max}=0$ for $n=0$. The model carries a precedence digraph for consistency with the companion missions; every statement here assumes it has no arcs.
• Implicit hypothesis. Theorems 1 and 5 assume every job fits alone ($r_{hj}\le s_h$), which the paper leaves unstated; without it no feasible schedule exists.
• The algorithm is a Lean definition following the page: the order is an argument (any nonincreasing order), "as early as possible" is the earliest start after $M_2$'s last job at which the resource constraint holds throughout, and the loop stops at the first move that does not strictly reduce $C_{\max}$.
• Optimality is always stated in full: feasibility plus a lower bound against every feasible schedule. No minimum is written as an infimum of a possibly empty set.
• Theorem 6 is stated with 0–1 slot assignments, the interpretation the paper gives to $x_{ijk}$; the page's constraint $\sum_{k=1}^{m}$ is read as $\sum_{k=1}^{n}$.
• Not formalized: the running times $O(ln^2+n^{5/2})$ (Theorem 1), $O(n\log n)$ (Theorem 5, including the phrase "This O(n log n) algorithm") and $O(n^3)$ (Theorem 6), which depend on a machine model the paper does not fix and, for Theorems 1 and 6, on cited matching and transportation algorithms.
• Ruled out: a formalization of the goal that proves optimality only against (a)–(c) schedules, against schedules with integer start times, or for one fixed tie-breaking order proves less than Theorem 5.

Contributions welcome: lemmas about step functions of resource usage on half-open intervals, a left-shifting lemma for unit-time schedules on two machines, and the exchange steps of Theorem 5 as separate lemmas.

Selected references

• J. Błażewicz, J.K. Lenstra, A.H.G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M.R. Garey, D.S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
• R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• S. Even, O. Kariv, An O(n^{2.5}) algorithm for maximum matching in general graphs, Proc. 16th IEEE FOCS (1975) 100–112. https://doi.org/10.1109/SFCS.1975.23