First raised for two variables by Ludwig Kraus in 1884 and stated in full generality by Ott-Heinrich Keller in 1939, the Jacobian conjecture asks something that sounds almost like freshman calculus: if a polynomial map from complex n-space to itself has a Jacobian determinant equal to a nonzero constant, must it be invertible by another polynomial map? That constant-Jacobian condition is precisely the algebraic shadow of the inverse function theorem, yet producing a polynomial — not merely analytic — inverse has resisted every attack for over eighty years. Shreeram Abhyankar championed the problem because it can be stated 'using little beyond a knowledge of calculus,' and Stephen Smale placed it sixteenth on his 1998 list of problems for the new century. Its notoriety is sharpened by a graveyard of published 'proofs' that later collapsed. Deep reductions exist — Bass, Connell, and Wright showed in 1982 that the general case reduces to maps of degree three — and the problem is equivalent, through work of Tsuchimoto, Belov-Kanel, and Kontsevich, to the Dixmier conjecture on the Weyl algebra. A formal statement anchors this famously slippery problem so that progress can be verified rather than merely believed.

The problem

(a) In a tennis match, you are the favorite, and win each point independently with probability $q\in(1/2,1)$. Let $n,m$ be odd positive integers greater than $1$. You have the choice between playing a best-of-$nm$ (i.e., you play $nm$ points and whoever wins the majority of points wins the match), or a best-of-$n$ of best-of-$m$'s (i.e., the match is won by winning the majority of $n$ "sets", and each "set" is won by winning the majority of $m$ points). Prove that your probability of winning the match is strictly greater by playing the best-of-$nm$.

(b) We now consider two generalizations: $m_1,\ldots,m_k$ are odd positive integers, while $n$ is any positive integer, with all integers being greater than $1$. You have the choice between playing a best-of-$nm_1\cdots m_k$, or a best-of-$n$ of "sets", which are best-of-$m_1$'s of "games", …, which are best-of-$m_k$'s of "points". In both cases, now that $n$ may be even, it is possible for the players to tie, in which case the match winner is determined by an independent fair coin. Prove again that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.

(c) We consider a further generalization where each completed "set" counts toward the match score in an independently random way:

• with probability $a$, the winner gains $1$ in the match score, as usual;
• with probability $b$, the set is ignored and does not count toward the match score;
• with probability $c$, the loser gains $1$ in the match score;

with $a+b+c=1$ and $a>c$, so players are still incentivized to win sets (previously we had $a=1$, $b=c=0$). This random scoring rule is applied once per completed set, at the outermost layer only: the games and points inside a set are decided by plain majorities, with no randomness, and only the set's final result is scored. If you choose to play the best-of-$nm_1\cdots m_k$, then each individual point counts as a set and is subject to the same randomness with probabilities $a,b,c$. Prove that your probability of winning the match is still strictly greater by playing the best-of-$nm_1\cdots m_k$ (the fair-coin-on-ties convention continues).

(d) Continue from part (c), but change the fair-coin-on-ties convention so that you only win the match if you have a strictly greater match score than your opponent. Assuming $b\ge1/2$, prove that your probability of winning the match is strictly greater by playing the best-of-$nm_1\cdots m_k$.

Source and connection to Dorner–Hardt

Florian E. Dorner and Moritz Hardt, Don't Label Twice: Quantity Beats Quality when Comparing Binary Classifiers on a Budget, ICML 2024. arXiv:2402.02249 (v3, 8 April 2026).

The paper asks how to spend a fixed budget of noisy crowdworker labels when comparing two binary classifiers: one label each for many data points, or several labels per data point aggregated by majority vote. It proves, via Cramér's theorem, that one label each is asymptotically optimal, and states the finite-sample version as an open conjecture (Section 5, Conjecture 1), still open in the April 2026 revision. Its Section 3 displays the finite-sample inequality for the independent, homogeneous-label case and verifies it numerically over about five billion parameter settings.

Part (d) of this mission with one level of sets is that Section 3 inequality in tennis language. A point is a single crowdworker label being correct ($q$ is the label accuracy); a set is a data point, whose test label is the majority of its $m$ labels; and the scoring rule is what the two classifiers do with that label. Writing $p$ for the worse classifier's accuracy and $p+\epsilon$ for the better one's, a set is scored to its winner when the better classifier alone matches the test label, ignored when the two classifiers agree, and scored to its loser when the worse classifier alone matches:

so that $a-c=\epsilon>0$, and $b\ge1/2$ always holds because two classifiers of accuracy at least $1/2$ agree on at least half the data. Substituting into the paper's Proposition 1 recovers its gap-indicator probabilities exactly: $\Pr(+1)=q\epsilon+p(1-p-\epsilon)$, $\Pr(-1)=(1-q)\epsilon+p(1-p-\epsilon)$. The paper's inequality also allows $n=1$ and $q=1$, which parts (c)–(d) exclude only because the inequality can fail to be strict at $b=0$ there; for $b\ge1/2$ the same argument covers those edge cases. The paper's Conjecture 1 as literally stated concerns a correlated-error setting (its Section 3.2) and is not claimed here.

Parts (a)–(c) go beyond the paper's setting: arbitrary nesting depth, a fair-coin tie rule, and no constraint on the ignore rate $b$. The hypothesis $b\ge1/2$ in part (d) cannot be dropped: with one level, $(a,b,c)=(0.9,0.1,0)$, $q=0.6$, $m=3$, $n=1$, the single best-of-3 finishes strictly ahead with probability $0.5832$ while three single points do so with probability $0.5761$.

Timeline

• Feb 2024 — arXiv v1; ICML 2024. Asymptotic theorem via Cramér; finite-sample statement conjectured; ~5·10⁹-configuration numerical sweep.
• Oct 2024 — arXiv v2.
• Apr 2026 — arXiv v3; conjecture still stated as open.
• Aug 2026 — private proof of the Section 3 inequality (strict win, $b\ge1/2$, one level) via exponential tilting of the tie probability.
• Sep 2026 — private proof of the fair-coin version with no constraint on $b$ (Bernstein degree elevation and a hypergeometric parity argument), then of the full four-part statement via a pairing lemma for player-symmetric rules. This mission formalizes that proof.

Conventions in the formal statement

"Greater than $1$" is read as $n\ge2$ and each $m_i\ge3$ odd; the list of set sizes in (b)–(d) is nonempty. Laws are functions $\mathbb Z\to\mathbb R$ and every probability is a finite sum — no measure theory. The goal theorem is the conjunction of the four parts.

Motivation

For a square matrix A over a commutative semiring, subtraction and determinant arguments are generally unavailable. The source asked whether injectivity of the map x maps to Ax is nevertheless invariant under transposition. The case n=2 was known, with n=3 presented as the first open size.

This mission turns CUHK-Shenzhen AI Math Problem 20, Transpose symmetry for injectivity over semirings, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

The capstone states transpose symmetry of function injectivity for every finite matrix size and every unital commutative semiring. In the current Prove2Me snapshot both the general theorem and the dimension-two supporting theorem are published and marked Proved. This mission concerns a resolved result, not an open general declaration. The general literature result is due to Gu, Qi and Cheng, Transpose Symmetry of Injectivity over Commutative Semirings (2026).

Significance

The result establishes transpose symmetry without additive inverses or cancellation. The current formal artifacts already record the finite-dimensional statement over arbitrary unital commutative semirings; users should inspect those exact statements and proof records before selecting extensions. The literature status and formal proof status are both resolved for the linked targets.

Difficulty

Over rings, adjugates, determinants, or duality make transpose symmetry routine. Over semirings, equality of alternating sums cannot be rearranged by subtraction, additive cancellation need not hold, and linear duals do not reflect injectivity. The successful proof must encode parity-separated minors and use injectivity itself to cancel vectors rather than scalars.

Suggested attack route

This mission is historical and solved in the literature. A Prove2Me solution can reconstruct the paper's proof with independently authored Lean code: isolate the even/odd minor algebra, verify the top separation identity, descend through matrix sizes, and derive coefficient equality. Generalizations to nonunital semirings and the parallel surjectivity theorem are natural follow-up nodes, provided their exact hypotheses match the paper.

Formalization scope

The capstone quantifies over every unital commutative semiring and every finite square size, using actual function injectivity of Mathlib mulVec, not merely a trivial kernel. The extra sizes zero, one and two do not weaken the original size-at-least-three question. Both linked theorem items are now Proved on Prove2Me. This update does not copy or redistribute any external repository source, and does not change the published Lean statements or proof identities.

Milestones

The linked dimension-two theorem is Proved. The general goal is also Proved. Any further generalization, such as a nonunital version or a surjectivity statement, would be a separately stated theorem rather than an unfinished part of either existing item.

Timeline and literature status

The source problem was added July 4, 2026. Sixuan Gu, Wei Qi, and Yaoyu Cheng posted a general proof on August 17, 2026, together with a Lean formalization. The mission records that rapid resolution rather than presenting the theorem as currently unknown.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

• Original problem
• Resolved 2026 paper
• Lean proof repository

Motivation

Invertible modules over a commutative semiring are Zariski-locally free, so local semirings have trivial Picard group. The source asks whether the ring-theoretic semilocal conclusion survives without subtraction: must every invertible module over a semiring with finitely many maximal ideals be free? If not, is the conclusion at least true for finite semirings?

This mission turns CUHK-Shenzhen AI Math Problem 19, Picard groups of semi-local or finite semirings, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

The main theorem asserts freeness for every invertible module over a commutative semiring with finite maximal spectrum. A separate milestone states the finite-semiring fallback. Both are positive formulations; a concrete counterexample to either resolves that target negatively and should motivate a corrected classification.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in semirings, Picard groups, invertible modules, finite semirings. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

Ring proofs use subtraction-sensitive k-ideal properties and decompositions into local factors that can fail for semirings. Finite indecomposable semirings need not be local and may have positive Krull dimension. Invertible modules are projective with strong duality, but familiar rank and determinant arguments may not survive additive noncancellation.

Suggested attack route

Formalize the known local-freeness proof from the evaluation isomorphism and study patching over finitely many principal opens. Identify exactly where partitions of unity require k-ideals. For finite semirings, enumerate idempotent matrices representing projective modules, impose the invertibility constraints, and seek either a reduction to principal rank-one modules or a minimal counterexample. Product decompositions and faithful-action lemmas should be reusable.

Formalization scope

The Lean targets use Mathlib's commutative semiring, maximal spectrum, module, invertible-module, and free-module notions. 'Semilocal' is encoded only as finiteness of MaximalSpectrum; no unproved decomposition theorem is assumed. The finite fallback assumes the underlying semiring type is finite but does not assume the module itself finite separately. Cardinality-only variants from the source are not the capstone.

The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.

Milestones

Resolve the finite-semiring statement, computationally or structurally, while developing the local-to-semilocal patching lemmas needed by the main theorem.

The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on June 24, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

• Original problem
• Facets of Module Theory over Semirings
• MathOverflow discussion

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.

[VM-STATUS-20260908-R05-PROVED]

Status update (2026-09-08): The root theorem OPG500Counterexample.eight_vertex_counterexample is now Proved by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. The historical text below describes the mission as it stood before formal closure.

Motivation and historical context

Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.

Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.

The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked candidate_only: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.

Setting

Let $G$ be a finite simple graph. A positive edge-length assignment is a function

such that $\ell(e)>0$ for every edge $e$. The length of a finite path or cycle is the sum of the lengths of its edges.

A simple cycle $C$ is $\ell$-geodesic when, for every pair of vertices $x,y$ on $C$, at least one of the two $x$–$y$ arcs of $C$ has length equal to the shortest-path distance between $x$ and $y$ in $G$. Equivalently, there is no $x$–$y$ path in $G$ whose length is strictly smaller than both $x$–$y$ arcs of $C$. The definition concerns vertices of the cycle and permits ties between shortest paths.

A simple cycle is peripheral when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.

Fix the graph $H$ on vertices $0,1,\ldots,7$. The vertices $0,1,2,3$ induce $K_4$. For each $i\in\{0,1,2,3\}$, set $y_i=7-i$ and join $y_i$ to exactly the three core vertices other than $i$. The four vertices $y_i$ are pairwise nonadjacent. Thus the frozen edge set is

The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.

Formalization targets

Main target: the universal eight-vertex obstruction

Formalize the following statement for the fixed graph $H$:

The existential cycle may depend on $\ell$. The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.

Supporting targets

The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of $H$, the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.

Significance

A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.

A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.

Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.

Difficulty

The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.

The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.

Formalization scope

The Lean development will use Fin 8 for the vertices of $H$ and a SimpleGraph representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.

The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.

Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.

Selected references

• A. Georgakopoulos and P. Sprüssel, Geodetic topological cycles in locally finite graphs, Electronic Journal of Combinatorics 16 (2009), R144. Section 3.1, Theorem 3.1; Section 5, Problem 3. https://arxiv.org/abs/0911.3999v1
• Open Problem Garden, Geodesic cycles and Tutte's Theorem, problem statement and vertex-based definition. https://www.openproblemgarden.org/op/geodesic_cycles_and_tuttes_theorem
• W. T. Tutte, How to draw a graph, Proceedings of the London Mathematical Society 13 (1963), 743–768. Cited as reference [18] by Georgakopoulos and Sprüssel for peripheral-cycle generation.
• Vibe Mathing, frozen OPG-500 candidate repository at commit a41fe59b4535851ea55f6e868e938b9aaf81e924. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924

Call $A \subseteq \mathbb{Z}/2^n\mathbb{Z}$ cube-free if no triple $x, y, z$ has all seven of $x$, $y$, $z$, $x+y$, $y+z$, $z+x$, $x+y+z$ inside $A$. The triple is unconstrained, so a degenerate one counts. Write $f(n)$ for the largest size of a cube-free subset.

The conjecture. $f(n) \le \frac{5}{8} 2^n$ for every $n$.

This is Conjecture 5.1 of Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of $\mathbb{Z}_{2^n}$, arXiv:1810.01225. It has been open since October 2018, and a 2026 journal paper still names it as conjectured: Yuchen Meng, On Cube-Free Problems, Electron. J. Combin. 33(1) (2026) #P1.16.

The constant is attained

The bound is sharp, and the extremal set is explicit: $A = \{v : v \bmod 8 \in \{1,3,4,5,7\}\}$, the odd residues together with those congruent to 4 mod 8. Its size is $2^{n-1} + 2^{n-3} = \frac{5}{8} 2^n$. In the layer language of Long and Wagner this is $C_3 = L_1 \cup L_3$.

What is known

The conjecture holds for unions of layers. That is Long-Wagner Theorem 1.10 at $d = 3$, and it is the largest class on which the conjectured constant is proved.

For arbitrary sets the best published unconditional bound is $f(n) < \frac{2}{3} 2^n$. Meng calls this bound "quite trivial" and gives it in one paragraph for every cyclic group, so it should not be read as progress toward $5/8$. The residual gap is exactly $\frac{2}{3} - \frac{5}{8} = \frac{1}{24}$, that is $2^n/24$ elements.

Small values are $f(1) = 1$, $f(2) = 2$, $f(3) = 5$, $f(4) = 10$, $f(5) = 20$, $f(6) = 40$, $f(7) = 80$, matching $2^{n-1} + 2^{n-3}$ from $n = 3$ on.

State those values honestly. They come from solver searches, Gurobi in Long and Wagner for $n \le 7$ and an independent SAT reproduction. The SAT half that matters, the unsatisfiability of "a cube-free set of size 81 exists at $n = 7$", is a solver claim with no proof certificate checked and no kernel check behind it. The witness half is verified: a set of exactly 80 elements was produced and re-checked cube-free. So $f(7) \ge 80$ is solid and $f(7) \le 80$ is not certified. Nothing in this mission rests on either.

What the items are

The goal item is the conjecture itself, for $n \ge 4$, and it is open. Every other item is a milestone that is proved mathematics, and the two closed instances $n = 4$ and $n = 5$ are stated separately because they are the only cases of the goal that a proof assistant has actually settled here.

The chain runs: the base case mod 8 by exhaustion, monotonicity under subsets, the bridge between the membership form and the Finset form of the forbidden configuration, sharpness, the odd-residue tight case, the layer-union theorem, the two-thirds bound, and then $n = 4$ and $n = 5$.

Notes on the formalization

Six definitions live in one definition item, Def_Z2nCubeFreeLayers: HasCube, CubeFree, config, ConfigFree, layerIdx and IsLayerUnion. layerIdx is written through the 2-adic valuation rather than through a congruence, because the congruence form leaves $0$ in no layer at all and needs the last layer special-cased.

CubeFree and ConfigFree are two encodings of the same condition and they are not definitionally equal, because config collapses duplicates on a degenerate triple. Their equivalence is a milestone rather than an assumption.

Formalize the corrected theory of flavor mixing angles in the su(3) Cartan sector of Cl(6,0), replacing the retired Killing-form/GUT normalization story. The mechanism: T3 and T8 commute, so mixing is carried not by their commutator but by the complete ordered products retained in grade 4. Milestone path: (M1) the grade-4 projection Pi4: Sym^2(A2) -> span{AB,AC,BC} is an isomorphism, with Pi4(e3^2) = -AB, Pi4(e3 e8) = (BC-AC)/sqrt 3, Pi4(e8^2) = (1/3)AB - (2/3)AC - (2/3)BC and tan(2 theta) = sqrt 3 (w-v)/(2u-v-w) for a retained grade-4 field G4 = u AB + v AC + w BC. (M2) the bridge: the primitive finite-T8 Cartan vector Phi = t e3 + e8 with t = sqrt 5 - 2 (the exact r = 16 closure) has grade-4 image exactly the rank-one family tensor phi phi^T; its traceless part is t[[-2,1],[1,2]], the Cabibbo family tensor up to one family-state sign, giving theta_C = arctan(sqrt 5 - 2) ~ 13.28 degrees; the grade-4 tensor has the same Sym2 structure as a left-handed Yukawa Gram operator M M^dagger. (M3, guarded goal) identify the r = 16 tensor with the relative left-family Yukawa tensor, closing the Sym2/Gram bridge. Foundational lemmas (A2 Cartan plane with [T3,T8] = 0, the complete 7-bracket su(3) table, grade-4 square residuals, grade-6 cubic channel) are landed in the LeanProofs repository and will be contributed as importable platform nodes ahead of the milestones. Recorded provenance: HAM memories #2848 (FullGradeCartanMixingTensorV1, 2026-09-14) and #3099 (CabibboGramSym2BridgeV1, 2026-09-17), proof DAG galaxy.proof-dag.v1 grade4-cartan-mixing.

Motivation

How few distinct distances can a planar point set determine? The near enemies of this mission are the closest competitors to the extremal configuration: points in no-three-collinear position (no line through three of them) and points lying on a common sphere — the lattice-sphere slice of Erdős–Füredi–Pach–Ruzsa is the motivating example. The bisector energy of a set counts ordered quadruples $(a,b,c,d)$ of points for which the pair $a,b$ and the pair $c,d$ have the same perpendicular bisector; it measures how far the set is from generic. Lund–Sheffer–de Zeeuw fixed the floor of this statistic: $2n(n-1)$ is a universal lower bound, and bisector injectivity is sufficient for equality. The Near Enemy theorem is the projection statement on top of it — every admissible set admits one generic projection whose image attains that floor, sits in general position, has zero rotation energy, and carries the whole distance-transport package.

Setting

Work with finite sets $P$ of points in the Euclidean plane (EuclideanSpace ℝ (Fin 2)), and in the transport direction with points in EuclideanSpace ℝ ι for a general finite index type. Following Lund–Sheffer–de Zeeuw, the bisector energy is

The rotation energy counts the ordered congruent quadruples whose difference vectors are neither equal nor opposite, so it discards the translation and half-turn channels and isolates the proper-rotation one. A linear map $T$ is projection-generic for a set $G$ when exactly two conditions hold: $T$ sends the difference of any two distinct points of $G$ to a nonzero vector, and for two distinct unordered pairs of $G$ the images never combine a parallel pair of differences with an orthogonal midpoint difference. Perpendicular bisectors, difference classes and distance images are all Finset operations.

Target

The mission goal is the spherical complete profile: for every finite set $G$ lying on a common sphere, in any dimension, there is a linear map $T$ to the plane whose image satisfies six conclusions at once —

together with injectivity of $T$ on $G$, general position of the image (no three collinear, no four cospherical), and exact distance transport. The projection is chosen per set — its very type depends on the ambient dimension — but a single projection delivers all six conclusions together, and that bundled form is what downstream incidence arguments consume.

Milestones ascend in five steps: the universal energy floor, the bisector-injectivity equality case, the attainment of the floor by projection-generic maps, the existence of such a map for every no-three-collinear set, and the no-three-collinear transport bundle that the goal then specialises to the spherical case.

Significance

Lund–Sheffer–de Zeeuw introduced the extremal picture for bisector energy at the level of the exact constant. In footnote 1 on p. 538 of the SoCG 2015 version (LIPIcs vol. 34, 537–552) they state that $\mathcal{E}(P) = 2n(n-1)$ when every distinct pair determines a distinct bisector, with the enumeration of the trivial quadruples that proves the floor. The universal asymptotic form $\mathcal{E}(P) = \Omega(n^2)$ is a remark in their §3.4.

This mission builds a complete machine-checked development of the floor, its attainment and the sufficiency direction, from first principles in Lean 4 over mathlib; the rotationEnergy statistic together with the rotationEnergy = 0 certificate for the projected image, where rotationEnergy(P) = 0 follows from the published "distance Sidon set" property; and a single generic projection of a given set that carries the bisector floor at the same time as the Erdős–Füredi–Pach–Ruzsa general-position package. Four of that bundle's six conjuncts are already in Erdős–Füredi–Pach–Ruzsa 1993, whose Theorem 3.1 supplies them.

Formalizing it matters because the argument composes analysis (generic projections obtained from nonvanishing of circle determinants), algebra (inner-product and determinant polynomial witnesses carrying linear_combination certificates) and counting (fiberwise difference-class tallies) — and the interfaces between the three must agree exactly. The projection-genericity and polynomial-witness lemmas are reusable for any Euclidean extremal formalization.

Difficulty

The hard step is keeping the projection generic through every predicate at once: a projection that preserves no-three-collinearity can still kill a circle determinant, or create a coincidence that the counting needs to keep distinct. The naive first idea — project along a random direction and hope — fails because each predicate forbids a different algebraic hypersurface of directions; the fix is a single simultaneous-avoidance argument over the union, with each forbidden set shown proper by an explicit polynomial witness. That step is the largest proof in the mission and carries its own milestone.

Formalization scope

Points are EuclideanSpace; finite sets are Finset; energies are ℕ-valued statistics. Generic projections are linear maps carrying the explicit two-clause ProjectionGeneric predicate, so there is no hidden regularity assumption. Dimension is a general ι with [Fintype ι] wherever the transport needs it. The goal's only hypothesis is membership of a common sphere; no-three-collinearity is derived from it rather than assumed, because a line meets a sphere at most twice. No statement is vacuous: explicit witnesses were checked in the kernel for the goal and for every milestone.

Welcome contributions: the converse of the equality case — bisector injectivity is proved here to be sufficient for the floor, and necessity is open in this development; sharpness examples beyond the Erdős–Füredi–Pach–Ruzsa configuration; and the incidence assembly that consumes this mission's output.

Selected references

• B. Lund, A. Sheffer and F. de Zeeuw, Bisector energy and few distinct distances, Proc. 31st SoCG 2015, LIPIcs vol. 34, 537–552, DOI 10.4230/LIPIcs.SOCG.2015.537; journal version Discrete Comput. Geom. 56 (2016), no. 2, 337–356, DOI 10.1007/s00454-016-9783-5, arXiv:1411.6868. Source of the bisector-energy statistic and its upper bounds. Footnote 1 on p. 538 of the SoCG version gives $\mathcal{E}(P) = 2n(n-1)$ for every set whose pairs have distinct bisectors, with the count of trivial quadruples that proves the floor; §3.4 (p. 545) gives $\mathcal{E}(P) = \Omega(n^2)$ for every set. The footnote is not in arXiv:1411.6868v1.
• P. Erdős, Z. Füredi, J. Pach and I. Z. Ruzsa, The grid revisited, Discrete Math. 111 (1993), 189–196, DOI 10.1016/0012-365X(93)90155-M — the lattice-sphere-slice configuration that gives this mission its name, and (proof of Theorem 3.1, p. 193) the generic planar projection that is injective, keeps general position and transports distances.
• J. Solymosi and T. Tao, An incidence theorem in higher dimensions, Discrete Comput. Geom. 48 (2012), no. 2, 255–280, DOI 10.1007/s00454-012-9420-x, arXiv:1103.2926, §5.1 — the canonical statement of the generic-projection trick this construction borrows. The same trick is used in J. Pach and F. de Zeeuw, Distinct distances on algebraic curves in the plane, Combin. Probab. Comput. 26 (2017), no. 1, 99–117, arXiv:1308.0177.
• McKenna, Lean formalization (mathlib-only, axiom-clean), lean-formalizations, module Geometry.Euclidean.NearEnemyTheorem.

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\}$.

Reversible Binary 2D Cellular Automata: Disproof of $R = 18$ and Lower Bound $R \ge 33,076,358$

Problem Statement & Context

A two-dimensional binary cellular automaton (CA) on the infinite grid $\mathbb{Z}^2$ with the standard $3 \times 3$ Moore neighborhood $M = \{-1,0,1\}^2$ updates configurations $c : \mathbb{Z}^2 \to \{0,1\}$ via a local rule $f : \{0,1\}^M \to \{0,1\}$ according to:

A local rule $f$ is reversible (or bijective) if its global map $F_f$ is a bijection of the configuration space $\{0,1\}^{\mathbb{Z}^2}$.

Let $R$ denote the exact number of reversible binary local rules on the $3 \times 3$ Moore neighborhood. A longstanding open conjecture asserted that $R = 18$, corresponding solely to the 18 trivial single-cell shifts and complemented shifts:

In this mission, we formally disprove $R = 18$ by constructing an explicit non-trivial conserved-landscape rule $f_\star$ whose global map $F_{f_\star}$ is an involution on $\mathbb{Z}^2$, proving $19 \le R$. We further extend this result to establish $R \ge 33,076,358$.

Ladder of Proven Bounds

Key Milestone Theorems

1. Theorem 1 (Trivial Rule Reversibility): All 18 single-cell shift and negated-shift rules are bijective global maps.
2. Theorem 2 (Conserved-Landscape Involution $f_\star$): The rule $f_\star$ complements a cell iff its W and SE neighbors are $1$ and the other six are $0$. $F_{f_\star} \circ F_{f_\star} = \text{id}$.
3. Theorem 3 (Non-Triviality & $19 \le R$): $f_\star$ differs from every trivial rule, establishing $19 \le R$ and disproving $R = 18$.
4. Theorem 4 (Constant Divergence Condition): Every reversible rule satisfies $f(\mathbf{0}) \ne f(\mathbf{1})$.

Motivation

A Costas array is a permutation matrix in which the difference vectors between distinct dots are pairwise distinct; such arrays are frequency-hopping patterns for sonar and radar (Costas, 1984). Rubio and Torres ask whether their $m$-dimensional version can stay Costas in every window of its periodic extension, and conjecture that this happens only in the smallest order.

Timeline. 1984: Taylor proves that 2D periodic Costas arrays have order $\le 2$. 2023: Rubio–Torres prove the odd-order and 3D cases, give $2\times2\times4$ examples, and state Conjecture 1.

Setting

Let $[n]=\{1,\dots,n\}$, $X=[a_1]\times\cdots\times[a_k]$, $Y=[b_1]\times\cdots\times[b_l]$ with all sides $\ge2$, and $\varphi:X\to Y$ a bijection; the dots are $(x,\varphi(x))\in\mathbb Z^{k+l}$. The array is Costas if the difference vectors between distinct dots are distinct, and periodic Costas if moreover, after repeating the dots periodically over $\mathbb Z^{k+l}$, the dots inside every translate $t+X\times Y$ have distinct difference vectors.

Formalization target

Conjecture 1: if $k\ge l\ge1$ and $\varphi$ defines a periodic Costas array, then

equivalently every $a_i=2$. The condition $k\ge l$ is a normalization ($\varphi^{-1}$ swaps the boxes).

Significance

A proof would give the multidimensional analogue of Taylor's theorem; a counterexample would give periodic distinct-difference patterns of non-power-of-two order.

Difficulty

The Rubio–Torres counting argument needs a bound that is available only when $Y$ is one-dimensional, which is why it stops at $m=3$. Computational evidence: an exhaustive window check reports that the $2\times3\times2\times3$ array with dots $(1,1,1,1),(1,2,1,2),(1,3,2,1),(2,1,1,3),(2,2,2,3),(2,3,2,2)$ is periodic Costas, which would disprove the conjecture.

Formalization scope

A point of $\mathbb Z^{k+l}$ is a pair $(x,y)$; boxes are 1-based; $\varphi$ is a total function $\mathbb Z^k\to\mathbb Z^l$ whose values off $X$ are unused. Differences are plain integer vectors (not reduced modulo the sides), windows range over all $t\in\mathbb Z^{k+l}$, and $k,l\ge1$ and sides $\ge2$ are part of the definition, so no degenerate case holds vacuously.

Selected references

• I. Rubio, J. Torres, Multidimensional Costas Arrays and Their Periodicity, IEEE Trans. Inf. Theory 69(8), 2023, 5032–5040. arXiv:2208.02378, DOI
• J. P. Costas, A study of a class of detection waveforms having nearly ideal range-Doppler ambiguity properties, Proc. IEEE 72(8), 1984, 996–1009.
• S. W. Golomb, H. Taylor, Constructions and properties of Costas arrays, Proc. IEEE 72(9), 1984, 1143–1163.

Motivation

Gustafson, Meinert and Melcher construct axisymmetric saddle points of the micromagnetic energy of a spherical shell in two ways (a heat flow, and continuation from an explicit solution at $\kappa=4$). Their Remark 3.18 conjectures that a single uniqueness statement identifies the two; it is problem 241 of the AIM open problem list.

Timeline. 2016: Kravchuk et al. propose the model. 2025: Gustafson–Meinert–Melcher construct the saddle points and state the conjecture.

Setting

For anisotropy $\kappa>0$ the energy of $m:S^2\to S^2$ is $\mathcal E_\kappa(m)=\frac12\int_{S^2}|\nabla m|^2+\kappa\,(1-(m\cdot x)^2)$. An axisymmetric field $m=(\sin h\cos\varphi,\ \sin h\sin\varphi,\ \cos h)$ with profile $h(\theta)$ is critical exactly when

The hemispheric class $H_{0,2}$ adds $h(0)=0$, $h(\pi)=2\pi$, $h(\pi-\theta)=2\pi-h(\theta)$.

Formalization target

For every $\kappa\ge4$ there is exactly one smooth profile in $H_{0,2}$ that solves (2.6) and induces a smooth map $S^2\to S^2$. The statement may be proved or disproved.

Significance

Uniqueness would identify the two constructions as one saddle branch; a counterexample would give further degree-zero critical points of $\mathcal E_\kappa$.

Difficulty

(2.6) is singular at both poles and $H_{0,2}$ is a two-point boundary condition, so standard ODE uniqueness does not apply, and the paper's comparison arguments only control solutions in the wedge $\theta\le h\le 2\theta$. Numerical evidence (shooting) finds at $\kappa=4$, besides $h=2\theta$, a second solution in the class with $h'(0)\approx3.899$ (similarly at $\kappa=5,8$), which leaves the wedge.

Formalization scope

Profiles are functions $h:\mathbb R\to\mathbb R$; all conditions, and the uniqueness, are imposed on $[0,\pi]$ only (values outside are unconstrained, so uniqueness on $\mathbb R$ would be trivially false). Smoothness is ContDiffOn ℝ ∞ on $[0,\pi]$. "Induces a smooth map" means the field extended to $\mathbb R^3\setminus\{0\}$ as a function of $x/|x|$ is $C^\infty$ there; this excludes profiles with a cone singularity at a pole. The paper's $H_{0,2}$ uses piecewise $C^1$ profiles; by its Corollary 2.7 it has the same solutions.

Selected references

• S. Gustafson, D. Meinert, C. Melcher, Saddle Point Configurations for Spherical Ferromagnets, preprint, 2025. arXiv:2509.05159
• V. P. Kravchuk et al., Topologically stable magnetization states on a spherical shell: Curvature-stabilized skyrmions, Phys. Rev. B 94, 144402, 2016. DOI
• AIM open problems list, problem 241. github.com/MColbrook/AIM

The Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge90$, also holds for every real $p\ge89$. This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-90 mission already covers every $p\ge90$, the new work is the range from 89 to 90.

The argument for $p\ge90$ was reached by tightening its estimates step by step, starting from 256. With its current choices those estimates stop working below 90, and nobody has yet found a way past that point. It is not known whether 90 is a real limit of the method or only of the choices made so far, so this mission is the smallest test of whether the cutoff can move at all. The accepted proof for $p\ge90$ and its research note are the natural starting point. The goal theorem below gives the exact statement.

This is an open entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 89 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
• Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 90.
• The accepted real coordinate bound for every real p ≥ 90.
• The accepted diagonal Schatten norm identity.

The Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge87$, also holds for every real $p\ge85$. This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the accepted cutoff-87 theorem already covers every $p\ge87$, the new work is the range from 85 to 87.

The cutoff came down from 90 to 87 in a day, through moona3k's proofs at 89, 88 and 87. The 89 proof reran the cutoff-90 argument with sharper, second-order estimates. A numerical model of that argument with retuned constants puts its limit between about 86.6 and 87.5: two of its steps pull the same parameter in opposite directions, and below that point no setting satisfies both. So reaching 85 is expected to need a new idea, not just tighter numbers. The goal theorem below gives the exact statement.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 85 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
• Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 87.
• The accepted real coordinate bound for every real p ≥ 87.
• The accepted diagonal Schatten norm identity.

This completed entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from 90 to 87. The goal is already proved in Lean on Prove2Me: for every real p ≥ 87, the foundation's cyclic constant K_p is the least constant that works for every triple of complex coordinate vectors in every finite dimension.

The statement includes arbitrary unequal-norm and zero triples, as well as dimension zero. It uses the foundation's unchanged definitions and combines admissibility with uniform optimality. This concerns complex diagonal matrices; it does not claim the corresponding result for general matrices or settle the conjecture for all p ≥ 2.

Proved goal and supporting result

• Sharp complex coordinate Hlawka constant for p ≥ 87: the goal, already Proved.
• The real coordinate Hlawka bound for p ≥ 87: the supporting milestone, already Proved.

The campaign template is instantiated with value 87. Both items reference the existing accepted theorems.

Proof route and attribution

The proof extends the accepted cutoff-90 Lean development by BrunoDCDO, adapting Ezzeri Esa's construction and analytic argument. The contributions at cutoffs 89, 88 and 87 were submitted by moona3k.

For p ≥ 88, the proof uses the accepted cutoff-88 result. On 87 ≤ p ≤ 88, it retains the localization, box-convexity and cyclic-averaging argument, with confinement parameter q₀ = 5351/15000, an improved cyclic witness (3/(4p))^(1/p), sharper Taylor estimates and exact rational polynomial certificates.

Campaign context

The foundation established cutoff 256; the supplied argument was formalized at cutoff 90. The subsequent accepted results extend the same formula to cutoffs 89, 88 and 87. This entry records the proved cutoff 87 on the campaign timeline; the campaign's cutoff-85 mission remains open.

• Sharp diagonal Hlawka campaign
• Foundation and proved cutoff 256

This entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from85 to84. For every real p≥84, the foundation's unchanged cyclic constant is the least constant comparing the triple deficit with the pair-deficit sum for every complex coordinate triple in every finite dimension.

The statement includes unequal and zero input vectors and dimension zero. It concerns complex diagonal matrices through their coordinate norms; it does not settle the conjectured cutoff2 or the full noncommutative matrix problem.

Goal and companion

• Exact complex cutoff84 goal.
• Real coordinate bound for p≥84, the supporting milestone.

Both exact proof submissions have been ACCEPTED by Prove2Me, and both theorem records are Proved. Their accepted sources match the submitted files and exact target statements in the pinned environment. This proposal references those existing verified results; the remaining steps are human submission and campaign moderation.

Construction and proof route

The construction is by Ezzeri Esa (GitHub savarin), with the accepted cutoff90 formalization by BrunoDCDO. Claude Opus5.5 produced moona3k's accepted89,88,87 work. Codex's accepted85 continuation and new84 extension reuse their verified generic calculus and transfer arguments.

On[84,85], an exact rational matrix sum-of-squares certificate proves a coupled radial energy estimate throughout a larger localization box. Residual estimates give nonnegative actual deficit Hessians and box convexity. Tight logarithm/Taylor bounds and exact positive Bernstein certificates localize every normalized failure. Orbit averaging and circle transfer prove the real and complex bounds, and the cyclic obstruction establishes leastness. The accepted85 development supplies the remaining tail.

Campaign context

The campaign began with cutoff256, followed by90,89,87,85. This entry instantiates its exact template with84 over the same foundation definitions.

Sharp diagonal Hlawka campaign

The Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge85$, also holds for every real $p\ge80$. This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-85 mission already covers every $p\ge85$, the new work is the range from 80 to 85.

The cutoff came down from 90 to 85 in two days, through moona3k's proofs at 89, 88, 87 and 85. The step to 89 sharpened the estimates of the cutoff-90 argument. The step to 85 added a new idea, a weighted pair-curvature and confinement estimate. How far that idea reaches is not known; 80 asks for five more units. The goal theorem below gives the exact statement.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 80 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
• Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 85.
• The accepted real coordinate bound for every real p ≥ 85.
• The accepted diagonal Schatten norm identity.