Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every $n\ge 3$, an eventual quantitative upper bound, the conclusion $f(n)=n^{1/2+o(1)}$, and the exact affirmative answer to the original upper-bound question.

Determine the exact second-order term in the least possible largest factor in a factorization of $n!$ into distinct integers exceeding $n$, with the proposed rational constant $4029639598/25970038185$.

How fast do multicolour Ramsey numbers grow? Write $R_k$ for the least $n$ such that every colouring of the edges of $K_n$ with $k$ colours contains a monochromatic triangle. The classical bounds, essentially unimproved for decades, place $R_k$ between $c^k$ and $e\cdot k!$, and Erdős asked repeatedly whether the truth is closer to the exponential lower end — his Problem 183 asks whether $R_k^{1/k}\to\infty$, i.e. whether the growth is genuinely superexponential.

This mission carries a complete Lean 4 formalisation resolving that question in the affirmative, with an explicit bound: $R_k \ge \left(\tfrac{1}{6e^{38}}\,k^{1/3}/\log k\right)^{k}$ for all sufficiently large $k$, from which $R_k^{1/k}\to\infty$ follows, together with the matching two-sided estimate $\log R_k = \Theta(k\log k)$ pinning the sharp coefficients. The argument is constructive: it builds triangle-free colourings by a recursive palette construction whose colour count grows fast enough to beat every exponential.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science, re-verified in this environment. Every node is proved — the mission is offered as a curated, closed campaign whose milestones map the attack path and whose lemmas are reusable foundations for further work on multicolour Ramsey theory.

Erdős and Simonovits conjectured that forbidding a finite family of graphs cannot reduce the extremal number by more than a constant factor compared with forbidding one of its members: for every finite nonempty family $\mathcal{F}$ whose members all contain a cycle, there should be some $F \in \mathcal{F}$ and $C>0$ with $\mathrm{ex}(n,F) \le C\,\mathrm{ex}(n,\mathcal{F})$ for all large $n$. The cycle hypothesis is essential — the folklore family $\{K_{1,2}, 2K_2\}$ already defeats the original formulation — and the corrected conjecture is Erdős problem #180.

This mission carries a complete Lean 4 formalisation refuting it, and refuting it quantitatively: there is a finite family $\mathcal{F}$ of connected bipartite graphs, each containing a cycle, with

The two bounds are separated by a polynomial factor $n^{1/48}$, so no member can dominate the family up to any constant. The family is $\mathcal{F} = \{C_4, C_6\} \cup \mathcal{J} \cup \mathcal{K}$, where $\mathcal{J}$ and $\mathcal{K}$ are the admissible quotients of two properly $2$-coloured templates built from the subdivisions of $K_{3,2}$ and $K_{3,3}$. The upper bound comes from counting short paths in an $\mathcal{F}$-free graph: excluding $\mathcal{J}$ bounds the number of vertices that fail to be centres of a subdivided $K_{3,3}$, and excluding $\mathcal{K}$ forces those vertices to form a vertex cover. The lower bound comes from incidence graphs of symplectic generalized quadrangles $W(q)$, with the characteristic of the underlying field chosen to suit the forbidden member — even $q$ for $\mathcal{J}$, odd $q$ for $\mathcal{K}$ — which is exactly the freedom a family bound does not have.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers"), re-verified in this environment. Every node is proved; the mission is offered as a curated, closed campaign whose definitions and lemmas are reusable foundations for further work in extremal graph theory.

A graph $H$ is $r$-degenerate if every nonempty subgraph of $H$ has a vertex of degree at most $r$. Erdős conjectured — this is Erdős problem #146 — that every fixed bipartite $r$-degenerate graph $H$ satisfies

The conjecture was known in several cases: when one bipartition class has maximum degree at most $r$, for $r$-degenerate blow-ups of trees, and, for $r = 2$, for grids and certain critical 2-degenerate graphs. The best general bound was the weaker $\mathrm{ex}(n,H) = O(n^{2-1/(4r)})$ of Alon, Krivelevich and Sudakov.

This mission carries a complete Lean 4 formalisation refuting it at $r = 2$.

Theorem. There exist a fixed connected bipartite 2-degenerate graph $H$ and constants $c, \varepsilon > 0$ such that

for all sufficiently large $n$. Since the conjectured bound at $r = 2$ is $O(n^{3/2})$, the excess is polynomial rather than constant, so the conjecture fails outright. A related conjecture of Erdős (problem #113) asserts that a bipartite graph is 2-degenerate if and only if $\mathrm{ex}(n,H) = O(n^{3/2})$; Janzer had already disproved the reverse implication, and this result refutes the forward one.

The construction. The counterexample $H$ is built in layers: starting from a layer $V_0$ of size $L_0$, each subsequent layer is $V_i = \binom{V_{i-1}}{2}$, and every vertex $\{a,b\} \in V_i$ is joined to its two parents $a, b \in V_{i-1}$. The result is connected, bipartite and 2-degenerate by construction, and is related to the complete degenerate graphs of Grzesik, Janzer and Nagy.

The lower bound comes from a sampled Hamming-ball graph. With $U = \{0,1\}^m$, two disjoint copies $U_L, U_R$ are joined whenever their Hamming distance is at most $k = \lfloor \tau m\rfloor$, and each vertex is retained independently with probability $p = 2^{-\beta m}$. The two parameters are governed by the thresholds

and the construction needs a sampling exponent with $A(\tau) < \beta < C(\tau)$. The lower threshold controls exclusion of the layered graph; the upper one controls whether the sampled host has more than $n^{3/2}$ edges.

Exclusion runs on a conditional-entropy functional $E(u,z) = \frac{1}{m}\sum_j H(Z_j \mid X_j, Y_j)$ over parent and child arrays. An array of conditional entropy $E$ has at most $2^{mME + O(m\log_2 M)}$ realisations, while requiring its $M = \binom{L}{2}$ children to survive sampling costs $2^{-\beta mM}$ — which dominates the $2^{mL}$ possible parent arrays whenever $E < \beta$. An embedding of $H$ would therefore have to raise a bounded entropy potential by a fixed amount at each layer, which is impossible after enough layers. A second-moment argument shows the sampled graph still has $\Omega(n^{3/2+\varepsilon})$ edges, and padding extends the construction to every sufficiently large order.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers", Sections 1.2 and 5–8), and re-verified in this environment: every node is proved from [propext, Classical.choice, Quot.sound] alone, and each staged statement's elaborated type was checked to be identical to the original declaration's. The mission is offered as a curated, closed campaign whose definitions and lemmas — binary entropy and the pair kernel, the layered construction, the Hamming-ball host and its retention measure — are reusable foundations for further work in extremal graph theory.

This is the companion result to Erdős problem #180, the Erdős–Simonovits compactness conjecture, which is formalised in the same source chapter and published as a separate mission.

Closed — negative resolution of Erdős Problems 96 and 97

Adam McKenna closed this mission on 13 September 2026 following Unit distances in convex polygons, by Liam Kruer, Jensen Kohlmeyer, and Liam Price. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.

Paper and complete Lean source. All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.

Do not start further proof attempts or solver runs for the affirmative conjectures. Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.

Historical mission description

Motivation

The mission is to prove the combined open goal

for finite point sets in strictly convex position in the Euclidean plane.

Why Problems 97 and 96 belong together

Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every nonempty convex-independent finite set then has a vertex with at most three neighbors at each positive radius, in particular at radius $1$. Delete that vertex and preserve convex independence. Apply the same step to every subset created by deletion until no points remain. Charge each unordered unit-distance pair to the first endpoint deleted. Each deleted vertex receives at most three charges, so an $n$-point set determines at most $3n$ unordered unit-distance pairs. This gives the Problem 96 bound and therefore $O(n)$. The package uses this one-way dependency; it does not seek a reverse implication.

Setting

Let $A\subset\mathbb R^2$ be finite. Strict convex position means that every point of $A$ is an extreme point of the convex hull of $A$. For $p\in A$, the pinned multiplicity at radius $r>0$ counts points $q\in A$ with $\lVert p-q\rVert=r$. Problem 97 asks for a point where no radius has four such other points. Problem 96 counts unordered pairs at distance $1$, then takes the supremum over convex-independent $n$-point sets.

The historical progression is part of the setting. Erdős’s 1946 paper posed an earlier three-neighbor version. His 1987 account reports Danzer’s convex nonagon in which every vertex has three equidistant witnesses, and asks about four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex configuration with the same unit distance at every vertex, placing the local question beside the unit-distance problem.

Target

The Problem 97 target is the canonical statement that every nonempty finite convex-independent $A$ has no four-equidistant-point property:

The Problem 96 target is the canonical asymptotic statement

where $U_c(n)$ is the supremum of the unordered unit-distance counts determined by convex-independent $n$-point sets. The bound is asymptotic; the Problem 97 route would give the stronger explicit bound $U_c(n)\le3n$ for every natural number $n$.

Significance

The package records a formal proof route joining a pinned geometric obstruction to a global extremal bound. A successful Problem 97 proof would immediately settle Problem 96 with the explicit constant $3$, while preserving the combinatorial meaning of the count. It also separates the historical three-neighbor constructions from the still-open four-neighbor assertion.

Difficulty

The source proof reduces Problem 97 to strong induction on $|A|$. Its counting engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib (2013). This engine forces every counterexample to have at least nine points; a finite geometric analysis excludes exactly nine points; and the remaining step must produce a removable vertex for every larger minimal counterexample. The removable-vertex statement carries the induction hypothesis that every strictly smaller nonempty convex 4-equidistant set is contradictory. That large-cardinality geometric step remains open, so both headline targets remain open. Finite computational certificates can support local cases but do not replace the universal geometric statement.

Counterexample routes

Problem 97 is open, so the mission also records the parallel negative route. The source formalization calls a nonempty convex-independent finite set with the four-equidistant property a Problem97.IsCounterexample. Constructing one such set would refute Problem 97 and therefore refute the mission's affirmative conjunction, regardless of whether Problem 96 remains true. The counterexample milestone keeps this resolution path visible beside the nonexistence proof. A successful witness must use exact coordinates or exact algebraic data from which Lean verifies both strict convex position and the four-equidistant property; a numerical approximation or a realizable incidence pattern alone is insufficient.

Problem 96 has its own negative route. Because its claim is asymptotic, one finite convex configuration cannot refute it. A counterexample must instead give convex-independent point sets at arbitrarily large cardinalities whose unit-distance counts exceed every proposed linear constant. The mission tracks this superlinear-family statement separately, together with a reduction from it to the exact negation of Problem 96. This keeps both possible outcomes visible: a direct or Problem-97-derived linear upper bound, and an explicit family proving that no such bound exists.

Formalization scope

The canonical source is pinned at commit 757d852766f377f7c1a0ffeeef6d3526bc0cb7a4. It contains the formal source statements for Problem 97 and Problem 96. The source repository reports closed proofs of the conditional bridge to the $3n$ bound (conditional three-times bound), the $|A|\ge9$ counting milestone (nine-point counting bound), and the exact nine-point exclusion (exact nine-point exclusion theorem). The remaining large-cardinality milestone is the removable-vertex step, with its minimality hypothesis retained. The current platform mission contains accepted transfers of the counting argument, the conditional bridge, and the exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make convex independence and the positive-radius condition explicit; no theorem is assumed inside a definition. Singletons and two-point sets are included in Problem 97, while Problem 96's counting definitions also include the empty set. The source repository uses Lean v4.27.0; these mission statements target the platform's v4.33.1. Source-proof transfer and revalidation remain separate work. The Lean declarations and proofs are this project's own formalization. The Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical provenance; they do not indicate that a paper proof was imported or machine-checked directly.

These source results establish the intended dependency graph: the P97 universal root feeds low-unit-degree extraction, strong induction, and then the P96 supremum bound. The platform mission records those contracts and milestones; it does not claim to have transplanted their proof bodies. The milestones include the two canonical roots, their conditional bridge, the |A| ≥ 9 count, the n = 9 exclusion, the |A| > 9 removable-vertex step, the documented Danzer nine-point three-neighbor example, the parallel goal of constructing a Problem 97 counterexample, and the superlinear-family route to a counterexample to Problem 96.

References

• Erdős, On Sets of Distances of n Points (1946), DOI.
• Erdős, Some Combinatorial and Metric Problems in Geometry (1987), scan.
• Fishburn–Reeds, Unit Distances Between Vertices of a Convex Polygon (1992), publisher record.
• Dumitrescu, On Distinct Distances from a Vertex of a Convex Polygon (2006), Springer record; provenance for the source counting method.
• Nivasch–Pach–Pinchasi–Zerbib, The Number of Distinct Distances from a Vertex of a Convex Polygon (2013), arXiv:1207.1266; provenance for the cap-witness refinements used by the source formalization.

What this mission proves, and what it does not. The goal theorem is the explicit upper bound $F(N)<3\sqrt N+1$ of Erdős, Lev, Rauzy, Sándor and Sárközy (1999) — a published result, now formally verified here. Erdős problem #131 itself is NOT solved by this mission. Erdős asked for the order of growth of $F(N)$, which is known only to lie between $N^{1/5}$ and $N^{1/4+o(1)}$ and remains open. A goal theorem reading Proved therefore means the 1999 bound is formalized, nothing more.

Motivation

Call a finite set of positive integers non-dividing if no element of it divides the sum of any nonempty collection of the other elements. The condition is easy to state and immediately restrictive: taking the collection to be a single element already forbids $a \mid b$, so a non-dividing set is primitive, and taking larger collections forbids a great deal more. Paul Erdős asked, with Lev, Rauzy, Sándor and Sárközy, how large such a set can be inside $\{1,\ldots,N\}$. Writing $F(N)$ for that maximum, the question is to determine the order of growth of $F(N)$. It remains unanswered, and the gap between what is known from above and from below is a full factor of $N^{1/20}$.

The problem sits at the meeting point of divisibility and additive combinatorics. Its upper bounds come from the theory of non-averaging sets, since every non-dividing set is non-averaging; its lower bounds come from explicit constructions. The two sides have been improved independently for twenty-five years without meeting.

Setting

Work inside $\mathbb{N}$. For a finite $A \subseteq \mathbb{N}$ and $a \in A$, write $A \setminus \{a\}$ for $A$ with $a$ removed. Say that $A$ is non-dividing when

Two conventions are forced. First, $S$ ranges over all nonempty subsets, singletons included, so primitivity is part of the property rather than an extra assumption. Second, $S$ must be nonempty: the empty sum is $0$ and every $a$ divides $0$, so admitting $S = \emptyset$ would leave no non-dividing sets at all.

Define the extremal function

A set is non-averaging if no element equals the average of some nonempty collection of the others. Every non-dividing set is non-averaging, which is the link through which the strongest upper bounds arrive.

Target

The goal is the explicit upper bound of Erdős, Lev, Rauzy, Sándor and Sárközy:

The question Erdős actually posed is stronger and remains open:

Significance

The bound above is the sharpest explicit constant in the literature, and it is the natural formalization target: it is a clean closed-form inequality valid for every $N$, with a self-contained combinatorial proof, and nothing about it is asymptotic.

Beyond it lies the open question. What is known:

• $F(N) > \exp\!\big((\sqrt{2/\log 2} + o(1))\sqrt{\log N}\big)$, due to Straus, which refuted Erdős's own initial guess that $F(N) < (\log N)^{O(1)}$.
• $F(N) \gg N^{1/5}$, from a construction Erdős credits to Csaba.
• $F(N) < 3N^{1/2} + 1$, the target above.
• $F(N) \le N^{1/4 + o(1)}$, from Pham and Zakharov's theorem on non-averaging sets. This settles Erdős's specific sub-question — whether $F(N) > N^{1/2 - o(1)}$ — in the negative.

So the truth lies between $N^{1/5}$ and $N^{1/4+o(1)}$, and which end is right is unknown.

Difficulty

The obvious argument gives almost nothing. Pigeonhole on partial sums shows $|A| \le \min A$: order the other elements arbitrarily, form the running sums, and if there are more of them than residues modulo $\min A$ then two agree, making a contiguous block sum divisible by $\min A$. That is genuinely all the elementary argument yields, and it is compatible with $|A|$ as large as $N$.

The difficulty is that the constraint is a statement about exponentially many subset sums, while the conclusion is about a single cardinality. Every strong bound known proceeds by discarding almost all of that information and keeping a structured fragment — contiguous blocks, or the averaging condition — and the loss at that step is exactly what separates $N^{1/5}$ from $N^{1/4}$. Improving either side appears to require using the divisibility conditions for several elements $a$ simultaneously, which no current argument does.

Formalization scope

Sets are Finset ℕ. The forbidden subsets are drawn from A.erase a, so the tested element never appears in the sum it is tested against, and they are quantified as members of (A.erase a).powerset rather than by the subset relation, which makes the property decidable — this is what allows an explicit finite witness to be checked by the kernel rather than asserted. $F(N)$ is a Finset.sup of cardinalities over the filtered powerset of Finset.Icc 1 N, so it is a total function with no junk-value caveats and lower bounds on it follow from exhibiting a single set.

The target inequality is stated over ℝ with Real.sqrt, matching the source's $3N^{1/2}+1$ rather than any integer rounding of it.

Timeline

• 1980s–1998. Erdős poses the problem repeatedly, initially conjecturing $F(N) < (\log N)^{O(1)}$.
• Straus. Disproves that guess, with $F(N) > \exp(c\sqrt{\log N})$.
• Csaba. A construction giving $F(N) \gg N^{1/5}$, credited by Erdős in 1997.
• 1999. Erdős, Lev, Rauzy, Sándor and Sárközy name the property non-dividing and prove $F(N) < 3N^{1/2} + 1$.
• 2024. Pham and Zakharov bound non-averaging sets, yielding $F(N) \le N^{1/4+o(1)}$ and answering Erdős's sub-question negatively.
• Open. The order of growth of $F(N)$, anywhere between $N^{1/5}$ and $N^{1/4+o(1)}$.

Selected references

• P. Erdős, V. Lev, G. Rauzy, C. Sándor, A. Sárközy, Greedy algorithm, arithmetic progressions, subset sums and divisibility, Discrete Mathematics 200 (1999), 119–135.
• H. T. Pham, D. Zakharov, Sharp bound for the Erdős–Straus non-averaging set problem, arXiv:2410.14624; Geom. Funct. Anal. (2025). Theorem 1: a non-averaging $A\subseteq[n]$ has $|A|\le n^{1/4+o(1)}$.
• R. K. Guy, Unsolved Problems in Number Theory, 3rd ed., Springer (2004), problem C16.
• Erdős problem #131, https://www.erdosproblems.com/131
• OEIS A068063, Maximum cardinality of a nondividing subset of $\{1,\ldots,n\}$.

Motivation

For every integer base $b\ge2$, a finite-prime weighted summability witness on a positive-integer host $H$ makes the reciprocal Mersenne series irrational on every infinite subset of $H$. A base-two witness gives that conclusion at every integer base. This is the source paper's proved Theorem 1; Erdős's unrestricted question for every infinite support remains outside its conclusion.

Setting

For an integer $b\ge2$, write $X_A(b)=\sum_{a\in A}(b^a-1)^{-1}$. Given a finite nonempty set $P$ of primes, let $h_P(a)=\prod_{p\in P}p^{v_p(a)}$ be the $P$-part of $a$, and set

All support elements are positive. The prime set specifies the weight, not which exponents may belong to the support; the weighted series must also converge.

Formalization targets

Theorem 1 has two clauses for an infinite positive-integer host $H$:

In each clause $P$ is finite and nonempty. In the second, one prime witness for $H$ is fixed before choosing $A$ and $b$. Taking $A=H$ recovers the two direct assertions. The public formal main item states both hereditary clauses and has an accepted proof in the pinned Lean 4.30 environment.

Significance

Since $h/(2^h-1)\le1$, this criterion includes reciprocal-summable supports. The paper also gives an explicit $A_\star$ with divergent reciprocal mass but finite weighted mass. The inherited conclusions let another formal result use one certified host for many infinite thinnings. The already proved Lean result makes the host criterion and its dependencies available for direct import; new applications can check the exact premise they need against the public statement.

Difficulty

Reciprocal summability cannot bound the tail for every weighted support. A faithful statement also has to preserve the different order of prime, subset and base quantifiers; dropping fixed-base inheritance changes Theorem 1.

Formalization scope

The formal support is a Set ℕ, and 0 ∉ H enforces positive exponents. FinitePrimeWeighted contains one finite nonempty set of primes and summability of its weighted terms. The public main item joins two accepted Lean results: the fixed-base hereditary theorem and the binary-host all-base theorem. These statements and their public definitions can be reused in the same pinned environment. The later no-cover host is a separate result; it is not a clause of Theorem 1 or the paper's $A_\star$ example. Will Cook is the named paper author; the paper discloses substantial AI-assisted research and drafting and does not claim independent human verification of every proof. Erdős’s earlier criterion and later platform contributions carry separate credit.

Selected references

• Will Cook, Weighted Support Criteria for Reciprocal Mersenne Subseries, Erdős Problem Note #257, 2026, Theorem 1.
• P. Erdős, On the irrationality of certain series, The Mathematics Student 36 (1968), 222–226 (issued 1969).