Algebraic Topology

Motivation

The smooth four-dimensional Poincaré conjecture asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of K3 — A New Problem List in Low-Dimensional Topology. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. Baykur–Kirby–Ruberman, Problem 4.1

Historical landmarks

• 1961: Smale proved that a closed smooth manifold homotopy equivalent to a sphere of dimension at least five is homeomorphic to that sphere. This is not a theorem that all such smooth manifolds are diffeomorphic to the standard sphere. Smale, Theorem A
• 1982: Freedman established the topological four-dimensional Poincaré theorem: a topological four-manifold homotopy equivalent to the four-sphere is homeomorphic to it. Freedman, Theorem 1.6
• 2026: The K3 problem list continues to distinguish this established topological result from the open smooth sphere problem. Problem 4.1, pp. 191–192

Setting

Let $S^4$ be the unit sphere in $ℝ^5$, with its standard stereographic smooth structure. A homeomorphism is a continuous bijection with continuous inverse; a diffeomorphism is a smooth bijection with smooth inverse. A smooth atlas is a collection of local Euclidean coordinates whose transition maps are smooth.

The manifold $M$ is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on $ℝ^4$. The given atlas is arbitrary: it is not defined by transporting the standard structure from $S^4$.

For a homeomorphism $e:N\to S^4$, let $\mathcal A_e$ denote the atlas transported from the standard sphere along $e$. A structomorphism for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate $\mathsf{SPC4Pullback}$ requires, for every given smooth atlas $\mathcal A$ on such an $N$ and every such $e$, a structomorphism between $(N,\mathcal A)$ and $(N,\mathcal A_e)$. It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, SPC4.lean, lines 53–81 and 211–221]

Formalization targets

Main open goal

For every manifold $M$ with the preceding hypotheses, the goal is

$$M\cong_{\mathrm{Top}}S^4 \quad\Longrightarrow\quad M\cong_{\mathrm{Diff}}S^4.$$

This is the source predicate $\mathsf{SPC4}$. Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.

Structural and literature milestones

The atlas formulation has the exact equivalence

$$\mathsf{SPC4}\quad\Longleftrightarrow\quad\mathsf{SPC4Pullback}.$$

The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence

$$\operatorname{Structomorph}(\mathcal G^{\infty},M,N) \simeq \operatorname{Diff}^{\infty}(M,N),$$

where $\mathcal G^{\infty}$ is the smooth coordinate-change groupoid for the common model. [Shin, SPC4.lean, lines 334–365; Bridge.lean]

Write $F_4$ for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:

$$M\simeq S^4\quad\Longrightarrow\quad M\cong_{\mathrm{Top}}S^4,$$

where $\simeq$ denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If $\mathsf{SPC4Homotopy}$ denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:

$$F_4\quad\Longrightarrow\quad (\mathsf{SPC4}\Longleftrightarrow\mathsf{SPC4Homotopy}).$$

Explicit standard-disk foundations form another track. For every $m\geq0$, they concern the manifold-with-boundary structure on $\overline B^{m+1}$, its boundary set $S^m$, and the smooth collar

$$c:S^m\times[0,1]\longrightarrow\overline B^{m+1}, \qquad c(u,t)=(1-t/2)u.$$

The collar is a closed embedding, has image

$$\{z\in\overline B^{m+1}:\|z\|\geq1/2\},$$

and satisfies $c(u,0)=u$, using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a $C^k$ map from a $C^k$ manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is $C^k$. These targets concern the actual disk smooth structure. [Shin, Disk.lean, lines 1076–1141 and 1263–1318]

Topological two-disk gluing

For each integer $m\geq0$, let $D^{m+1}=\overline B^{m+1}$ be the closed unit disk in $\mathbb R^{m+1}$ and let $\varphi:S^m\to S^m$ be any homeomorphism of its boundary. The twisted double identifies the boundary point $u$ in a left copy of the disk with $\varphi(u)$ in a right copy. With the quotient topology, the target is

$$X_\varphi:=\bigl(D^{m+1}_L\sqcup D^{m+1}_R\bigr)/(u_L\sim\varphi(u)_R) \quad\cong_{\mathrm{Top}}\quad S^{m+1}.$$

This statement is published as SP4Gluing.twistedSphere_homeomorphic. The theorem and its supporting continuity and injectivity lemmas have accepted Lean proofs contributed by carlok. All three accepted proofs have also been checked locally with their proved dependencies. It concerns these explicit topological quotients, not arbitrary homotopy spheres or a prescribed smooth structure.

Seam–interior smooth compatibility

For every regional chart base point, the open-bicollar and left-interior transitions are smooth in both directions. Right-interior-to-seam smoothness requires smooth $\varphi^{-1}$; the reverse requires smooth $\varphi$. The single compatibility target concerns exact overlap sources, combining four source results internally. It provides neither a global smooth-manifold instance nor smooth standardness. [Shin, Hemisphere.lean, lines 2439–3577]

Significance

A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.

The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and Freedman's topological theorem remains unproved in this formal development despite its published mathematical proof.

The topological two-disk gluing result identifies the homeomorphism type of these quotients for every boundary homeomorphism and every disk dimension at least one. The accepted formalization supplies a global topological comparison for this explicit quotient. It does not resolve the comparison with a prescribed smooth structure or recognition of general smooth four-manifolds.

Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by wamlart: orbit augmentation, region homology budgets, two-corner homology budgets, the Laurent mass threshold, and mass-two positivity. No theorem currently connects their completion to a proof or disproof of $\mathsf{SPC4}$. They are exploratory tools, not established milestones in a proof of the main goal.

Difficulty

A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.

Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a smooth gluing or recognition theorem for an arbitrary prescribed smooth structure, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.

Formalization scope

The sphere goal quantifies over Type in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order $\infty$. Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.

The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every $m\geq0$, so their dimensions are $m+1\geq1$. The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.

The separate source assertion SPC4Ball is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product diffeomorphism is not a current target; its chart instances serve only as constructor support. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.

Selected references

• R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., K3 — A New Problem List in Low-Dimensional Topology, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. Author PDF.

• Michael Hartley Freedman, The topology of four-dimensional manifolds, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. DOI; primary-article scan.

• Stephen Smale, Generalized Poincaré's Conjecture in Dimensions Greater Than Four, Annals of Mathematics 74 (1961), 391–406, Theorem A. DOI; primary-article scan.

• Ryan Shin, SPC4.lean, Bridge.lean and Disk.lean, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc, e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302, 889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e.

• Ryan Shin, Hemisphere.lean, unpublished Lean source file, 2026, declaration twistedSphereHomeoSphere; source SHA-256 c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828. Published topological two-disk gluing target; the recovered local construction is checked; the accepted proof and its two supporting lemmas were contributed by carlok.

Motivation

In fair division, a value may be assigned to each interval that a cut produces. If the value is continuous in the interval's endpoints, an equal-value partition is a natural target. Some valuations are nonnegative and additive, but a difference of competing measures or a signed utility need have neither property. Avvakumov and Karasev establish equal-value partitions even when the value changes sign and is not additive, provided it vanishes on degenerate intervals. Their result is used by Bogomolnaia and Moulin in work on guarantees for fair division. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.

The paper identifies earlier special cases: a nonnegative valuation follows from the Knaster–Kuratowski–Mazurkiewicz theorem; prime-power numbers of parts with a valuation of varying sign were known through degree-theoretic results; additive valuations admit an elementary argument. The remaining case permits a sign-changing, nonadditive valuation and an arbitrary positive number of parts. The authors distinguish this from an envy-free division problem with separate valuations for several players, which they state remains open outside prime-power cases. Avvakumov and Karasev, p. 2; Avvakumov and Karasev, Envy-free division using mapping degree; Meunier and Zerbib.

Setting

Write $\mathcal I$ for the set of all subsegments $I=[a,b]$ of $[0,1]$ with $0\le a\le b\le1$. An interval may be degenerate, meaning $a=b$. A real-valued function $f$ on $\mathcal I$ is continuous when its value varies continuously with the two endpoints. The required boundary condition is $f([a,a])=0$ for every $a\in[0,1]$. No sign, monotonicity, or additivity condition is imposed. A partition into $m$ parts is a sequence $0=x_0\le x_1\le\cdots\le x_m=1$, so its parts $[x_{j-1},x_j]$ may also be degenerate. Avvakumov and Karasev, Theorem 1.1, pp. 1–2.

The intermediate setting is a nice multivalued function. Its graph is a compact subset $Z$ of $\mathcal I\times(-1,1)$. The graph separates the bottom $\mathcal I\times\{-1\}$ from the top $\mathcal I\times\{1\}$ inside the cylinder $C=\mathcal I\times[-1,1]$: those two sides lie in different connected components of $C\setminus Z$. A representation of a nice graph is a continuous real function $\varphi$ on $C$ that is negative on the bottom, positive on the top, and whose zero set is the graph. The paper passes between graphs and representations in Lemma 2.2. Avvakumov and Karasev, Definition 2.1 and Lemma 2.2, p. 2.

For a prime $p$, a segment $I=[a,b]$, and a value $y$, a zero partition is a sequence $a=x_0\le\cdots\le x_p=b$ such that $\varphi([x_{j-1},x_j],y)=0$ for each $j=1,\ldots,p$. The set $Z_p(\varphi)$ contains exactly those pairs $(I,y)$ that admit a zero partition. This is the projection to the cylinder of the paper's simultaneous-solution set $S$ for labeled partitions. Avvakumov and Karasev, equation (4.1) and Claim 4.4, pp. 7–9.

Formalization targets

The goal is Theorem 1.1: for every positive integer $m$ and every continuous $f$ satisfying the degenerate-interval condition, there are possibly repeated cut points with a common value:

$$0=x_0\le x_1\le\cdots\le x_m=1,\qquad f([x_0,x_1])=\cdots=f([x_{m-1},x_m]).$$

The theorem is already posed as the Open platform statement FairGuarantees.DivideChoose.theorem_of_4; this mission references that exact statement as its goal. It supplies the paper's supporting statements, including Lemma 2.2 on graph representations, Claim 4.4 on separation by projected zero partitions, and the prime-step Lemma 2.3. The latter asserts that, when $\varphi([a,a],y)=y$, there is a represented nice graph with the same degenerate identity whose zeros each yield a zero partition for $\varphi$. The milestone list includes the fixed-segment and continuous-family statements used to characterize $Z_p(\varphi)$, and equation (4.2) describing its degenerate boundary. Avvakumov and Karasev, Lemmas 2.2–2.3, pp. 2–3; Claims 4.3–4.4 and equation (4.2), pp. 8–9.

Significance

The theorem guarantees equal values for any positive number of consecutive parts under only endpoint continuity and the zero-on-degenerates condition. It covers valuations for which nonnegative or additive special-case results give no conclusion. It also provides the theorem invoked in the fair-guarantee application cited by the authors. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.

The mathematical result was proved in the paper; the platform's theorem statement remains Open and lacks a machine-checked proof there. Formalizing the paper's intermediate claims makes its topological assumptions and its treatment of degenerate parts explicit. The definitions of a separating graph, its representation, and zero partitions can also be reused for related partition problems. The present mission states the paper's prime-step targets, leaving the proofs and the underlying equivariant topology as work for solvers.

Difficulty

For a fixed signed valuation, continuity alone does not select one common value that works across every piece of an arbitrary partition. The nonnegative case has a simplex-covering argument, but that argument does not directly control values of both signs. In the paper's general case, the difficult claim is that the projected simultaneous-zero set separates an entire cylinder, even as the segment varies. Its source proof requires a mod-$p$ statement for a space of labeled partitions and control of the resulting solution set. A further boundary issue arises on degenerate segments: a representation of the projected graph must satisfy $\psi([a,a],y)=y$, not merely have the right zeros. Avvakumov and Karasev, pp. 2, 7–10.

Formalization scope

Lean represents $I=[a,b]$ by the endpoint pair $(a,b)$ with $0\le a\le b\le1$. The cylinder uses the closed value range $[-1,1]$; a nice graph lies in its open interior $(-1,1)$. Functions are total Lean functions, but only their values on this cylinder enter the definitions and results. Continuity is required on the cylinder. Separation uses connected components of its complement, as in Definition 2.1, and explicitly requires the bottom and top to avoid the graph. This prevents a graph containing a boundary side from satisfying separation vacuously.

Every prime-step claim assumes $p$ prime, the representation's strict boundary signs, and the degenerate identity. Zero partitions have exactly $p$ consecutive parts whose endpoints are pinned to the original segment; repeated cuts are allowed. The goal reference likewise permits degenerate parts and assumes $m\ge1$. The projected set is defined through existence of an ordinary ordered partition, independent of how the paper labels partitions in its configuration space. The needed existing Lean notions include ContinuousOn, IsCompact, connectedComponentIn, finite index types, and Nat.Prime. A complete proof development also needs results about the paper's labeled-partition complex, equivariant cycles and transverse maps. Contributions establishing that reusable topology, as well as proofs of the stated milestones, are within scope. Avvakumov and Karasev, §§2–4.

Selected references

• Sergey Avvakumov and Roman Karasev, Equipartition of a Segment, Mathematics of Operations Research, 2023. arXiv:2009.09862v4.
• Anna Bogomolnaia and Hervé Moulin, Guarantees in Fair Division: General or Monotone Preferences, 2019. arXiv:1911.10009v3.
• Sergey Avvakumov and Roman Karasev, Envy-Free Division Using Mapping Degree, Mathematika 67, 2021. arXiv:1907.11183.
• Frédéric Meunier and Shira Zerbib, Envy-Free Cake Division Without Assuming the Players Prefer Nonempty Pieces, Israel Journal of Mathematics 234, 2019. arXiv:1804.00449.

Motivation

The diffeomorphism group $\mathrm{Diff}(M)$ of a closed smooth manifold $M$, topologized so that two diffeomorphisms are close when they and all their derivatives are uniformly close, is a basic invariant of the smooth structure of $M$. Its set of path components $\pi_0\,\mathrm{Diff}(M)$ is the group of isotopy classes of diffeomorphisms (the smooth mapping class group), and its higher homotopy groups classify smooth fibre bundles with fibre $M$. For spheres, the natural comparison is with the orthogonal group $O(n+1)$ of isometries of the round metric, which sits inside $\mathrm{Diff}(S^n)$.

S. Smale asked how far $\mathrm{Diff}(S^n)$ is from $O(n+1)$. The question was settled positively in dimensions $n \le 3$ and has been studied extensively in dimensions $n \ge 5$, where surgery theory and pseudo-isotopy theory apply. Dimension $4$ is the remaining case, and it is where the least is known. The question is recorded on the Open Problem Garden (problem page) with importance "Outstanding".

Timeline.

• 1959 — S. Smale: $\mathrm{Diff}(S^2) \simeq O(3)$.
• 1963 — M. Kervaire and J. Milnor compute the groups $\Theta_n$ of homotopy spheres; combined with Cerf's pseudo-isotopy theorem this computes $\pi_0\,\mathrm{Diff}(S^n)$ for many $n \ge 5$ (for example $\pi_0\,\mathrm{Diff}^+(S^6) \cong \Theta_7 \cong \mathbb Z/28$).
• 1970s — the Cerf–Morlet comparison theorem $\mathrm{Diff}(D^n) \simeq \Omega^{n+1}(PL_n/O_n)$ (Kirby–Siebenmann, Foundational Essays).
• 1978 — F.T. Farrell and W.C. Hsiang compute $\pi_i\,\mathrm{Diff}(D^n)\otimes\mathbb Q$ in a stable range of degrees for large $n$.
• 1983 — A. Hatcher: $\mathrm{Diff}(S^3) \simeq O(4)$ (the Smale conjecture).
• 2007 — R. Budney: $\mathrm{Diff}(D^4)$ is a $5$-fold loop space, via little cubes acting on spaces of long knots.
• 2018 — T. Watanabe: $\pi_*\,\mathrm{Diff}(D^4)\otimes\mathbb Q \ne 0$; the $4$-dimensional Smale conjecture is false (arXiv:1812.02448).

Whether $\mathrm{Diff}(D^4)$ is connected is still unknown.

Setting

Write $\mathbb R^n$ for Euclidean space with the Euclidean norm, $D^n$ for the closed unit ball and $S^n \subset \mathbb R^{n+1}$ for the round unit sphere.

• $\mathrm{Diff}(D^n)$ is the group of diffeomorphisms of the $n$-ball rel boundary. Concretely it is the group of smooth diffeomorphisms $f\colon \mathbb R^n \to \mathbb R^n$ with $f(x) = x$ whenever $\|x\| \ge 1$. Two such maps are close when their $k$-th derivatives are uniformly close for every $k$ (the $C^\infty$ topology). The base point is the identity.
• $\mathrm{Diff}(S^n)$ is the group of all smooth diffeomorphisms of $S^n$ (orientation-preserving or orientation-reversing), with the $C^\infty$ topology. Derivatives are measured through the degree-one homogeneous extension $x \mapsto \|x\|\, f(x/\|x\|)$, taken on the sphere.
• $O(n)$ is the group of real orthogonal $n\times n$ matrices with the matrix topology.
• $X \simeq Y$ means that $X$ and $Y$ are homotopy equivalent. $\pi_0 X$ is the set of path components, and $\pi_i(X,x)$ is the $i$-th homotopy group. $\Omega^k(Y,y)$ is the $k$-fold loop space, the space of maps $[0,1]^k \to Y$ sending the boundary of the cube to $y$.

The source states that $\mathrm{Diff}(S^4) \simeq O(5) \times \mathrm{Diff}(D^4)$, so the homotopy type of $\mathrm{Diff}(S^4)$ is determined by that of $\mathrm{Diff}(D^4)$.

Formalization targets

Goal: connectivity of $\mathrm{Diff}(D^4)$

$$\pi_0\,\mathrm{Diff}(D^4) = 0, \qquad\text{i.e. } \mathrm{Diff}(D^4) \text{ is path-connected.}$$

The source asks to "determine some (any?) homotopy or homology groups of $\mathrm{Diff}(D^4)$" and singles out connectivity as unknown. The goal is the yes/no question for $\pi_0$. It can be settled either way: a proof shows that every diffeomorphism of $D^4$ rel boundary is isotopic to the identity, and a disproof exhibits one that is not.

Milestones

1. $\mathrm{Diff}(S^4) \simeq O(5)\times\mathrm{Diff}(D^4)$ (problem statement).
2. $\mathrm{Diff}(D^4) \simeq \Omega^5(Y,y)$ for some pointed space $(Y,y)$ (Cerf–Morlet, Budney).
3. $\mathrm{Diff}(D^4)$ is not contractible (Watanabe).
4. $\mathrm{Diff}(S^2) \simeq O(3)$ (Smale).
5. $\mathrm{Diff}(S^3) \simeq O(4)$ (Hatcher).
6. $|\pi_0\,\mathrm{Diff}(S^6)| = 56$ (Kervaire–Milnor and Cerf).
7. For $2 \le i < \min\{\tfrac{n-4}{3}, \tfrac{n-7}{2}\}$: $\pi_i\,\mathrm{Diff}(D^n)\otimes\mathbb Q \cong \mathbb Q$ if $n$ is odd and $4 \mid i+1$, and $0$ otherwise (Farrell–Hsiang).

Significance

The result itself. A positive answer would mean $\pi_0\,\mathrm{Diff}(S^4) \cong \mathbb Z/2$, detected by orientation alone, matching dimensions $1$, $2$ and $3$. A negative answer would give an exotic diffeomorphism of $S^4$: one that is topologically isotopic to the identity (by the Alexander trick) but not smoothly isotopic. By the Cerf–Morlet theorem, $\pi_0\,\mathrm{Diff}(D^4) \cong \pi_5(PL_4/O_4)$, so the question is equivalent to a question about the homotopy of $PL_4/O_4$, the space controlling smoothings of PL $4$-manifolds. The source lists the smooth $4$-dimensional Schoenflies problem as a related problem.

Formalizing it. No part of this theory is currently formalized in Lean or Mathlib: there is no $C^\infty$ topology on diffeomorphism groups and no known homotopy equivalence involving one. The milestones are classical theorems (Smale 1959, Hatcher 1983, Kervaire–Milnor 1963, Farrell–Hsiang 1978, Watanabe 2018). Formalizing any of them is new work, independent of the open goal.

Difficulty

In dimensions $\ge 5$, $\pi_0\,\mathrm{Diff}(D^n)$ is computed by combining Cerf's pseudo-isotopy theorem with the $h$-cobordism theorem. Both rely on the Whitney trick, which fails in dimension $4$. In dimension $4$ one also cannot reduce to a lower-dimensional problem as Smale and Hatcher did. The known invariants that detect non-trivial elements of $\pi_*\,\mathrm{Diff}(D^4)$ (Watanabe's configuration-space integrals) are rational and live in positive degrees, so they say nothing about $\pi_0$. Smale's and Hatcher's arguments for $n = 2, 3$ rely on understanding spaces of embedded spheres in $S^n$ of one lower dimension; the corresponding spaces of $3$-spheres in $S^4$ are not understood, so those arguments do not carry over.

Formalization scope

All statements import the single definition file SmaleDiffS4_Basic and live in the namespace SmaleDiffS4.

• DiffDisk n is the subtype of Mathlib's Diffeomorph 𝓘(ℝ, ℝⁿ) 𝓘(ℝ, ℝⁿ) ℝⁿ ℝⁿ ∞ (smooth = C^∞) of maps fixing every point of norm $\ge 1$. Its topology is induced by the family of iterated derivatives iteratedFDeriv ℝ k f, $k \in \mathbb N$, each with the topology of uniform convergence on $\mathbb R^n$. This "identity outside the open ball" model is the standard model of $\mathrm{Diff}(D^n \text{ rel } \partial)$ and is homotopy equivalent to the "identity on the boundary" and "identity near the boundary" variants.
• DiffSphere n is Mathlib's Diffeomorph (𝓡 n) (𝓡 n) (sphere 0 1) (sphere 0 1) ∞ on the unit sphere of $\mathbb R^{n+1}$. Its topology is induced by the iterated derivatives of the radial extension, restricted to the sphere and uniformly topologized.
• OrthGroup n is Matrix.orthogonalGroup (Fin n) ℝ with the subspace topology.
• Homotopy equivalence is ContinuousMap.HomotopyEquiv. $\Omega^5$ is GenLoop (Fin 5) Y y, $\pi_0$ is ZerothHomotopy, and $\pi_i$ is HomotopyGroup (Fin i). $\pi_i\otimes\mathbb Q$ is TensorProduct ℤ ℚ (Additive π_i), and "$\cong\mathbb Q$" is stated as $\mathbb Q$-rank $1$.
• The Farrell–Hsiang milestone covers only $i \ge 2$, where $\pi_i$ is abelian in Mathlib. It includes the parity hypothesis "$n$ odd" of the original theorem, which is lost in the source page's rendering.

A trivializing formalization is ruled out: the topology is the genuine $C^\infty$ topology rather than the discrete or indiscrete one, and the goal is not vacuous because DiffDisk 4 is nonempty (it contains the identity).

A complete development needs reusable infrastructure: the $C^\infty$ topology and topological-group structure on diffeomorphism groups, isotopy extension and fibration theorems (Cerf–Palais), restriction to a disc, and the Alexander trick. Contributions of this infrastructure as separate theorems are welcome.

Selected references

• Open Problem Garden, What is the homotopy type of the group of diffeomorphisms of the 4-sphere? (posted 2009). http://www.openproblemgarden.org/op/what_is_the_homotopy_type_of_the_group_of_diffeomorphisms_of_the_4_sphere
• S. Smale, Diffeomorphisms of the 2-sphere, Proc. Amer. Math. Soc. 10 (1959), 621–626. https://doi.org/10.1090/S0002-9939-1959-0112149-8
• M. Kervaire, J. Milnor, Groups of homotopy spheres I, Ann. of Math. 77 (1963), 504–537. https://doi.org/10.2307/1970128
• R. Kirby, L. Siebenmann, Foundational Essays on Topological Manifolds, Smoothings, and Triangulations, Princeton University Press, 1977.
• F.T. Farrell, W.C. Hsiang, On the rational homotopy groups of the diffeomorphism groups of discs, spheres and aspherical manifolds, Proc. Sympos. Pure Math. 32 (1978), 403–415.
• A. Hatcher, A proof of a Smale conjecture, $\mathrm{Diff}(S^3)\simeq O(4)$, Ann. of Math. (2) 117 (1983), 553–607. https://doi.org/10.2307/2007035
• R. Budney, Little cubes and long knots, Topology 46 (2007), 1–27. https://arxiv.org/abs/math/0309427
• T. Watanabe, Some exotic nontrivial elements of the rational homotopy groups of $\mathrm{Diff}(S^4)$, 2018. https://arxiv.org/abs/1812.02448

Motivation

For a $k$-regular graph $G=(V,E)$ on $n$ vertices, the Expander Mixing Lemma (Alon–Chung 1988; see the survey of Hoory, Linial and Wigderson 2006) says that for any vertex sets $A,B$, the number of edges between them is close to its expected value: $\bigl||E(A,B)|-k|A||B|/n\bigr|\le\rho\sqrt{|A||B|}$, where $\rho$ is the largest absolute value of a nontrivial eigenvalue of $kI-\Delta^+$. The deviation, called the discrepancy of $A$ and $B$, measures how random-like the graph is. It is one of the basic tools of spectral graph theory and of the theory of expanders.

Higher-dimensional expansion asks the same questions for simplicial complexes, where the role of edges is played by $d$-dimensional cells. Parzanchevski, Rosenthal and Tessler (Combinatorica 35, 2015) prove, for complexes with a complete skeleton, a Cheeger inequality and a Mixing Lemma: the number of $d$-cells with one vertex in each of $d+1$ disjoint vertex sets is controlled by the spectrum of the upper Laplacian. The Mixing Lemma is the result of this mission. In the same paper it yields a lower bound on Gromov's geometric overlap (Gromov 2010) of complexes with a small spectral spread.

Setting

Let $V=\{0,1,\dots,n-1\}$ and $d\ge1$. A $d$-dimensional complex with a complete skeleton $X$ contains every set of at most $d$ vertices as a cell, together with a set $X^d$ of $d$-cells, each a set of $d+1$ vertices. Cells are oriented by the increasing order of their vertices.

A $(d-1)$-form is a real function on the $d$-element subsets of $V$; the space $\Omega^{d-1}$ carries the inner product $\langle f,g\rangle=\sum_\sigma f(\sigma)g(\sigma)$. Similarly $\Omega^{d-2}$ consists of functions on $(d-1)$-subsets ($\Omega^{-1}=\mathbb R^{\{\varnothing\}}$ when $d=1$) and $\Omega^d$ of functions on $d$-cells. Writing $\sigma_i$ for the $i$-th vertex of $\sigma$, the co-boundary operators are $(\partial^*_j f)(\sigma)=\sum_{i}(-1)^i f(\sigma\setminus\sigma_i)$ (for $j=d$ only on $\sigma\in X^d$), and the boundary operators are $(\partial_j g)(\sigma)=\sum_{v\sim\sigma} g(v\sigma)$, the sum over vertices $v\notin\sigma$ with $\{v\}\cup\sigma$ a cell, where $v\sigma$ is the oriented cell $[v,\sigma_0,\sigma_1,\dots]$.

The upper, lower and full Laplacians on $\Omega^{d-1}$ are

$$\Delta^+=\partial_d\partial^*_d,\qquad \Delta^-=\partial^*_{d-1}\partial_{d-1},\qquad \Delta=\Delta^++\Delta^-.$$

The $(d-1)$-cycles are $Z_{d-1}=\ker\partial_{d-1}$, and the exact forms are $B^{d-1}=\operatorname{im}\partial^*_{d-1}$; they are orthogonal complements in $\Omega^{d-1}$. Write $\mathbb P_{Z_{d-1}}$ and $\mathbb P_{B^{d-1}}$ for the orthogonal projections. For vertex sets $A_0,\dots,A_d$, $F(A_0,\dots,A_d)$ is the set of $d$-cells with exactly one vertex in each $A_i$.

For $\alpha\in\mathbb R$ the operator $\alpha I-\Delta^+$ preserves $Z_{d-1}$, and

$$\rho_\alpha=\max\bigl\{|\mu|\;:\;\mu\text{ an eigenvalue of }(\alpha I-\Delta^+)|_{Z_{d-1}}\bigr\}=\bigl\|(\alpha I-\Delta^+)|_{Z_{d-1}}\bigr\|.$$

Formalization targets

Goal: Theorem (1.4), the Mixing Lemma (p. 16)

For every $\alpha\in\mathbb R$ and any pairwise disjoint vertex sets $A_0,\dots,A_d$ (not necessarily a partition),

$$\left|\,|F(A_0,\dots,A_d)|-\frac{\alpha\cdot|A_0|\cdots|A_d|}{n}\right|\le\rho_\alpha\cdot\bigl(|A_0|\cdots|A_d|\bigr)^{\frac d{d+1}}.$$

The parameter $\alpha$ is free; the introduction's Theorem 1.4 (p. 4) is the case $\alpha=k$, the average degree of a $(d-1)$-cell, and is included as a companion item.

Milestones

The milestones follow the proof of §4.3 and the facts of §§2–3 that it uses:

1. the chain-complex identity $\partial_{d-1}\partial_d=0$ and its dual, so $B^{d-1}\subseteq\ker\Delta^+$ (p. 6), and $B^{d-1}=Z_{d-1}^\perp$ (p. 6);
2. Proposition 3.2: $\Delta^+_{\overline X}=nI-\Delta_X$ for the complement complex (3.4), and $\Delta^-=n\,\mathbb P_{B^{d-1}}$ (3.5);
3. for the signed indicator forms $\varphi=\delta_{A_0,A_1,\dots,A_{d-1}}$ and $\psi=\delta_{A_d,A_1,\dots,A_{d-1}}$: the norm identity (4.5), the count $\langle\varphi,(D-\Delta^+)\psi\rangle=|F(A_0,\dots,A_d)|$ (4.6), its $\alpha$-shift (4.7), the splitting (4.8), the main term (4.9), the spectral bound (4.10)–(4.11);
4. the asymmetric bound $\rho_\alpha\sqrt{|A_0||A_d|}\,|A_1|\cdots|A_{d-1}|$ and the geometric-mean step that symmetrizes it.

Significance

For $d=1$ the theorem is the Expander Mixing Lemma of graphs. For $d\ge2$ it shows that a complex whose upper Laplacian has its nontrivial spectrum concentrated near $\alpha$ distributes its $d$-cells evenly across any $d+1$ disjoint vertex sets, with a bound that depends on the set sizes only through $(\prod|A_i|)^{d/(d+1)}$. The paper uses it to bound the geometric overlap of such complexes from below (Corollary 1.6), and to show that random Linial–Meshulam complexes (Linial–Meshulam 2006) have small discrepancy.

The result is proved in the paper. To the knowledge of this mission, neither it nor the underlying signed simplicial Laplacians with their Hodge decomposition on a complete skeleton has been formalized. The formalization produces the boundary and co-boundary operators, the three Laplacians, the identity for the complement complex, and the projection formula for $\Delta^-$, all of which are standard in the spectral theory of complexes and reusable well beyond this result.

Difficulty

Each step of the proof is a finite computation, but the steps are sign-sensitive. The count (4.6) relies on the orientation conventions: $\psi$ replaces only the first block of $\varphi$, and the off-diagonal terms of $\Delta^+$ carry the signs that make $\varphi(\sigma)\psi(\sigma')=+1$ on neighbouring cells. Proposition 3.2 (1) and (3) are identities between explicit matrices indexed by $d$-subsets that hold only because the skeleton is complete. The spectral step needs the orthogonal decomposition $\Omega^{d-1}=B^{d-1}\oplus Z_{d-1}$, invariance of $Z_{d-1}$ under $\Delta^+$, and the spectral theorem for the restriction. A direct transcription of the graph argument does not apply: the operators act on $(d-1)$-forms rather than on functions on vertices, and the expected count $\alpha\prod|A_i|/n$ is not visible from $\Delta^+$ of $X$ alone.

Formalization scope

Vertices are Fin n. A complex is the structure Complex n d holding its $d$-cells, so the complete skeleton is built in; forms are EuclideanSpace ℝ over the subtype of $k$-element subsets of Fin n, oriented by the order of Fin n. All boundary and co-boundary operators are defined by their formulas, not as adjoints of one another. The standing assumption $d\ge1$ is added to every statement. The disjoint sets $A_0,\dots,A_d$ form an arbitrary pairwise-disjoint family, some possibly empty; no partition and no bound $n\ge d+1$ is assumed. The exponent $d/(d+1)$ is a real power of a nonnegative real.

$\rho_\alpha$ is not defined as a maximum or supremum: the goal is stated for every real $\rho$ that bounds $|\mu|$ for all eigenvalues $\mu$ of $\alpha I-\Delta^+$ on $Z_{d-1}$, which is equivalent to the statement for $\rho_\alpha$. Trivializing formalizations are ruled out by construction: forms cannot be supported outside $d$-subsets (such a form would be a spurious cycle), an empty eigenvalue set cannot be read through a default sSup value, the boundary operators carry orientation signs, and disjoint families are not confused with partitions.

Contributions are welcome at every milestone, in particular a general library for signed boundary operators on finite complexes, the identity $\partial\partial=0$, and the Hodge-type decomposition of forms, which are reusable for the Cheeger inequality of the companion mission and for other work on high-dimensional expanders.

Selected references

• O. Parzanchevski, R. Rosenthal, R. J. Tessler, Isoperimetric inequalities in simplicial complexes, Combinatorica 35 (2015); arXiv:1207.0638v3 (2013). https://arxiv.org/abs/1207.0638 , https://doi.org/10.1007/s00493-014-3002-x
• N. Alon, F. R. K. Chung, Explicit construction of linear sized tolerant networks, Discrete Mathematics 72 (1988). https://doi.org/10.1016/0012-365X(88)90189-6
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bulletin of the AMS 43 (2006). https://doi.org/10.1090/S0273-0979-06-01126-8
• N. Linial, R. Meshulam, Homological connectivity of random 2-complexes, Combinatorica 26 (2006). https://doi.org/10.1007/s00493-006-0027-9
• M. Gromov, Singularities, expanders and topology of maps. Part 2: From combinatorics to topology via algebraic isoperimetry, Geometric and Functional Analysis 20 (2010). https://doi.org/10.1007/s00039-010-0073-8

Motivation

For a finite graph, the Cheeger constant measures how hard it is to cut the vertex set into two pieces, and the spectral gap of the graph Laplacian measures how fast random walks mix. The two Cheeger inequalities (Dodziuk 1984; Alon and Milman 1985; Alon 1986) bound each quantity by a function of the other, and they underlie the theory of expander graphs, with uses in derandomization, error-correcting codes and the analysis of Markov chains.

High-dimensional expanders extend this theory from graphs to simplicial complexes. Linial and Meshulam (2006) and Gromov (2010) introduced combinatorial and topological notions of expansion for complexes; the spectral side is Eckmann's discrete Hodge theory (1944), in which each dimension carries its own Laplacian. Parzanchevski, Rosenthal and Tessler (arXiv:1207.0638, Combinatorica 2015) defined a $d$-dimensional Cheeger constant $h(X)$ through partitions of the vertices into $d+1$ blocks and proved the analogue of the upper Cheeger inequality, $\lambda(X)\le h(X)$, for complexes with a complete skeleton. This mission formalizes that theorem.

Setting

Let $V=\{0,1,\dots,n-1\}$ and $d\ge1$. A finite $d$-complex with a complete skeleton $X$ on $V$ consists of all subsets of $V$ with at most $d$ elements together with a set $X^d$ of $(d+1)$-element subsets, the $d$-cells. A set of $j+1$ vertices is a $j$-cell; $X^{d-1}$ is therefore the set of all $d$-element subsets.

Each cell is oriented by the increasing order of its vertices, $\sigma=[\sigma_0,\dots,\sigma_j]$ with $\sigma_0<\dots<\sigma_j$. The space $\Omega^{j}$ of $j$-forms consists of the real functions on $j$-cells, with inner product

$$\langle f,g\rangle=\sum_{\sigma\in X^{j}}f(\sigma)g(\sigma).$$

The co-boundary $\partial_d^*:\Omega^{d-1}\to\Omega^d$ and the boundaries $\partial_d:\Omega^d\to\Omega^{d-1}$, $\partial_{d-1}:\Omega^{d-1}\to\Omega^{d-2}$ are

$$(\partial_d^*f)(\tau)=\sum_{i=0}^d(-1)^i f(\tau\setminus\tau_i),\qquad (\partial_j g)(\sigma)=\sum_{v\sim\sigma}g([v,\sigma_0,\dots,\sigma_{j-1}]),$$

where $v\sim\sigma$ means that $v\notin\sigma$ and $\{v\}\cup\sigma$ is a cell, and $[v,\sigma_0,\dots]$ equals $(-1)^k$ times the increasingly oriented cell when $v$ has $k$ smaller vertices in $\sigma$. The upper Laplacian is $\Delta^+=\partial_d\partial_d^*$ on $\Omega^{d-1}$, and $Z_{d-1}=\ker\partial_{d-1}$ is the space of $(d-1)$-cycles.

The spectral gap is the least eigenvalue of $\Delta^+$ on the cycles (Definition 2.1):

$$\lambda(X)=\min\operatorname{Spec}\big(\Delta^+|_{Z_{d-1}}\big).$$

For sets $A_0,\dots,A_d\subseteq V$, let $F(A_0,\dots,A_d)$ be the set of $d$-cells with exactly one vertex in each $A_i$. The Cheeger constant is (Definition 1.1)

$$h(X)=\min_{V=\coprod_{i=0}^dA_i}\frac{n\cdot|F(A_0,\dots,A_d)|}{|A_0|\cdot|A_1|\cdots|A_d|},$$

the minimum over partitions of $V$ into nonempty sets $A_0,\dots,A_d$. For $d=1$, $Z_0$ is the space of functions summing to zero, $\Delta^+$ is the graph Laplacian, and $h$ is the usual Cheeger constant $\min_{A}\,n|E(A,\bar A)|/(|A||\bar A|)$.

Formalization targets

Goal: Theorem 1.2 (Cheeger Inequality)

$$\lambda(X)\le h(X)$$

for every finite $d$-complex $X$ with a complete skeleton on $n\ge d+1$ vertices.

Milestones

1. The chain-complex identity $\partial_{d-1}\partial_d=0$ (p. 6).
2. The form $f$ of (4.1), built from a partition, is a $(d-1)$-cycle (p. 12).
3. $\partial_d^*$ is the adjoint of $\partial_d$: $\langle\partial_dg,f\rangle=\langle g,\partial_d^*f\rangle$ (p. 6).
4. Rayleigh's principle (4.2): $\lambda(X)\langle f,f\rangle\le\langle\Delta^+f,f\rangle=\langle\partial_d^*f,\partial_d^*f\rangle$ for $f\in Z_{d-1}$ (p. 12).
5. $\langle f,f\rangle=n\prod_{i=0}^d|A_i|$ for the form (4.1) (p. 13).
6. (4.3): $|(\partial_d^*f)(\sigma)|$ equals $n$ for $\sigma\in F(A_0,\dots,A_d)$ and $0$ for the other $d$-cells (p. 13).
7. $\langle\partial_d^*f,\partial_d^*f\rangle=n^2|F(A_0,\dots,A_d)|$ (p. 14).

Milestones 2 and 5–7 hold for every partition, not only a minimizing one.

Significance

The result. Theorem 1.2 shows that a large spectral gap forces every partition of the vertices into $d+1$ blocks to be crossed by many $d$-cells, so spectral information certifies combinatorial expansion of a complex. The paper uses it with the spectral analysis of Gundert and Wagner to show that Linial–Meshulam random complexes $X(d,n,C\log n/n)$ have Cheeger constant of order $\log n$ for large $C$ (Corollary 1.3). The paper also shows that the converse direction fails: a triangulation of the Möbius strip has $h(X)=1\tfrac14$ but $\lambda(X)=0$, so no lower bound of the form $C\cdot h(X)^m\le\lambda(X)$ holds.

Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof requires a signed simplicial chain complex with explicit orientations, the adjoint relation between boundary and co-boundary, and a Rayleigh-quotient bound for a symmetric operator on an invariant subspace. These are the basic tools for any further formal work on spectral high-dimensional expansion, including the Mixing Lemma of the same paper (the companion mission of this series).

Difficulty

The graph proof plugs a two-valued test function into the Rayleigh quotient. In dimension $d$ the test vector must be a $(d-1)$-cycle, and an indicator of a block is not one. The paper's form (4.1) assigns to a $(d-1)$-cell whose vertices meet $d$ distinct blocks the size of the missing block, with the sign of a permutation of the blocks. Showing that this form is a cycle and that its co-boundary has absolute value exactly $n$ on $F(A_0,\dots,A_d)$ and $0$ elsewhere is a case analysis over how the vertices of a cell fall into blocks, and every case depends on the orientation signs. A convention error in any of the operators or in the form makes one of these identities fail. A second, smaller difficulty is that $\lambda(X)$ is a minimum over the spectrum on a subspace, so the Rayleigh bound must be proved for $\Delta^+$ restricted to $Z_{d-1}$, which it preserves.

Formalization scope

• Vertices are Fin n; a complex is a structure holding its $d$-cells as Finset (Finset (Fin n)), each of size $d+1$; the complete skeleton is built into the type. Complexes without $d$-cells are allowed.
• Forms are EuclideanSpace ℝ over the subtype of $k$-element vertex sets, so no form is supported on sets of the wrong size. $\Omega^d$ is modelled on all $(d+1)$-element sets; $\partial_d^*$ vanishes off $X^d$ and $\partial_d$ ignores values there.
• Orientation is by the order of Fin n; the sign of vertex $v$ in cell $\tau$ is $(-1)^{\#\{w\in\tau:w<v\}}$. Boundary and co-boundary are both defined by their formulas; their adjointness is milestone 3.
• The spectral gap is not defined by sInf. The goal states that some eigenvalue $\mu$ of $\Delta^+$ on $Z_{d-1}$ (a nonzero cycle $f$ with $\Delta^+f=\mu f$) is at most the Cheeger ratio of every partition, which is equivalent to $\lambda(X)\le h(X)$. A partition is a family A : Fin (d+1) → Finset (Fin n) of nonempty, pairwise disjoint sets covering the vertices.
• Added hypotheses: $d\ge1$ (the Laplacians act on $\Omega^{d-1}$) and $n\ge d+1$ (presupposed by the paper, since $h$ minimizes over partitions into $d+1$ nonempty sets; for $n\le d$ the cycle space is $0$).
• Ruled out: forms supported off the $d$-element sets (they would be spurious cycles with eigenvalue $0$), an eigenvalue set read through sInf (empty sets give $0$), unsigned boundaries (for which $\partial\partial\ne0$), cocycles $\ker\partial_d^*$ in place of cycles $\ker\partial_{d-1}$ (on which $\Delta^+$ is zero), and arbitrary disjoint families in place of partitions (empty blocks give ratio $0$).
• Needed infrastructure: sign bookkeeping for faces of sorted finsets, the spectral theorem for symmetric operators on a finite-dimensional inner product space restricted to an invariant subspace (Mathlib's LinearMap.IsSymmetric), and counting cells by blocks of a partition. The chain-complex and adjointness lemmas are reusable in any formal development of simplicial Hodge theory; contributions there are welcome.

Selected references

• O. Parzanchevski, R. Rosenthal, R. J. Tessler, Isoperimetric inequalities in simplicial complexes, Combinatorica 35 (2015). arXiv:1207.0638v3, doi:10.1007/s00493-014-3002-x
• B. Eckmann, Harmonische Funktionen und Randwertaufgaben in einem Komplex, Comment. Math. Helv. 17 (1944), no. 1, 240–255.
• N. Alon, V. D. Milman, λ₁, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985), 73–88. doi:10.1016/0095-8956(85)90092-9
• N. Linial, R. Meshulam, Homological connectivity of random 2-complexes, Combinatorica 26 (2006), 475–487. doi:10.1007/s00493-006-0027-9
• A. Gundert, U. Wagner, On Laplacians of random complexes, Proceedings of the 2012 Symposium on Computational Geometry, ACM, 2012, 151–160.
• M. Gromov, Singularities, expanders and topology of maps. Part 2: From combinatorics to topology via algebraic isoperimetry, Geom. Funct. Anal. 20 (2010), no. 2, 416–526.

Motivation

A classifying-space problem asks whether a natural complex captures a group without additional higher homotopy. The source addresses the finite-rank Artin problem through the lifted spherical-cell complex. The source is OpenAI's September 2026 manuscript.

Setting

An Artin group is presented by alternating braid relations from a Coxeter matrix. A subset of generators is spherical when its associated Coxeter parabolic subgroup is finite. Lifted cells pair a group element with such a subset, with incidence determined by reduced coset words.

Formalization targets

$$\operatorname{ContractibleSpace}(\operatorname{SalvettiCover}(M))\qquad\text{for every Coxeter matrix }M\text{ on finite }S.$$

For every Coxeter matrix M indexed by a finite type S of standard generators, the topological space SalvettiCover(M) is contractible. The Artin group Artin(M) is the free group on S modulo the braid relators, one for each ordered pair (s,t): the alternating word s t s t ... of length M(s,t) times the inverse of the alternating word t s t s ... of the same length. A subset T of S is spherical when the standard parabolic subgroup of the Coxeter group generated by the simple reflections in T is finite. A lifted cell is a pair (a,T) of an Artin group element and a spherical subset. One lifted cell (a,T) is a face of (b,U) when T is contained in U and there is a word w in letters of U that is reduced in the Coxeter group (its Coxeter length equals the word length), is of minimal length in its coset with respect to the parabolic subgroup generated by T, and satisfies a = b times the image of w in the Artin group. The preorder on lifted cells is the reflexive transitive closure of this face relation, and SalvettiCover(M) is the geometric realization, as a topological space, of the nerve of that preorder viewed as a category.

The goal is OAI.HarmonicArtin.salvetti_cover_contractible.

Significance

The goal makes the full topological realization contractible, rather than only asserting vanishing of a selected homotopy group. It supplies a precise target for the covering-space component of the source. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Local spherical pieces need not automatically fit into a globally contractible realization. The face relation and its transitive closure must retain the interaction between Artin words and Coxeter length.

Formalization scope

SalvettiCover is the geometric realization of the nerve of the lifted-cell preorder. The generator type is finite but need not be equipped with a chosen enumeration. The mission preserves this published model instead of substituting a different complex.

The shared definitions are supplied by HarmonicArtin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Harmonic heights and the Artin K(pi,1) conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Topological entropy measures orbit complexity, whereas the induced map on homology measures algebraic growth. The mission asks for a C¹ self-map where these two measurements violate the proposed entropy lower bound. The source manuscript presents the surrounding research claim.

Setting

The counterexample manifold is S¹×(S²)^(q+1), realized as a product of standard Euclidean spheres. A C¹ self-map is continuous and locally agrees, through the standard embedding, with a C¹ ambient map. Real singular homology provides the induced linear action.

Formalization target

Construct q>0 and such a nonbijective f with

$$h_{top}(f)=0,\qquad\exists v\in H_2(M;\mathbb R)\setminus\{0\},\ f_*v=2v,$$

and prove 0<log 2≤log ρ_total(f), with 5≤2q+3.

The selected formal target is OAI.Problem340.exists_C1_entropy_counterexample.

Significance and status

The spectral-radius gap is an explicit conclusion, supported by an eigenvalue-two homology class. The target concerns noninvertible C¹ maps. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Algebraic expansion in homology must coexist with zero topological orbit entropy. Merely displaying a low-entropy subsystem would not establish zero entropy on the whole manifold.

Formalization scope

The goal uses Dynamics.coverEntropy on the entire manifold, taking values in EReal. Its total homological spectral radius is defined through real pairs representing complex eigenvalues over all homology degrees. The manifold family, ambient-extension C¹ condition and nonbijectivity are fixed parts of the statement.

Selected references

• OpenAI, A C^1 Counterexample to the Entropy Conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

A model structure on a category specifies weak equivalences, fibrations and cofibrations so that the category carries a homotopy theory. Thomason showed that the category $\mathbf{Cat}$ of small categories carries a model structure Quillen equivalent to simplicial sets, so that ordinary categories model all homotopy types of spaces (Thomason 1980). Its weak equivalences are the functors whose nerves are weak homotopy equivalences.

Strict higher categories have a nerve too: Street's orientals $\mathcal O_m$ give the Street nerve $N_n$ of a strict $n$-category (Street 1987). The higher-dimensional Thomason model-structure conjecture of Ara and Maltsiniotis asks for the analogue of Thomason's theorem for strict globular $n$-categories for every $1\le n\le\infty$ (Ara–Maltsiniotis 2014; Ara 2023, §§9.2.5–9.2.6; Guetta–Maltsiniotis 2024). Strict higher categories are already known to describe the homotopy category of spaces after localization (Gagna, below); the conjecture asks for the full model structure, with lifting and factorization on all strict $n$-categories.

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims the conjecture in every dimension. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Timeline

• 1980 — Thomason constructs the model structure on $\mathbf{Cat}$ by transfer along $c\,\mathrm{Sd}^2\dashv\mathrm{Ex}^2N$, introducing Dwyer maps (Cahiers 1980).
• 1987 — Street defines orientals and the nerve of strict $\omega$-categories (JPAA 1987).
• 1999 — Cisinski corrects the retract argument in Thomason's properness proof (Cahiers 1999).
• 2007/2016 — Worytkiewicz, Hess, Parent and Tonks propose the 2-dimensional structure (JPAA 2007), with a later corrigendum (JPAA 2016).
• 2010 — Fiore and Paoli construct a Thomason structure on $n$-fold categories (AGT 2010).
• 2014 — Ara and Maltsiniotis develop the transfer theorem, settle dimension 2, and isolate sufficient conditions for all $n$ (Adv. Math. 2014).
• 2018 — Gagna shows that strict $n$-categories model homotopy types after localizing at nerve weak equivalences (Adv. Math. 2018).
• 2023–2024 — Ara's habilitation records the remaining pushout condition and the conjecture; Guetta and Maltsiniotis state the $\omega$-dimensional conjecture.
• 2026 — The OpenAI preprint claims the conjecture for every $1\le n\le\infty$ (Theorem 1.1, p. 2).

Setting

A strict globular $\omega$-category has a set of cells, source and target operations $s_k,t_k$ in each dimension, and associative, unital compositions $\ast_k$ along $k$-dimensional boundaries satisfying the interchange law; every cell has finite dimension. A strict $n$-category is one whose cells above dimension $n$ are identities; $n\mathbf{Cat}$ denotes the category of small strict $n$-categories and strict functors ($n=\infty$ means $\omega\mathbf{Cat}$). No invertibility is assumed.

The Street nerve $N_n:n\mathbf{Cat}\to\mathbf{sSet}$ has $(N_nX)_m=\mathrm{Hom}(\mathcal O_m,X)$, with left adjoint $c_n$. With barycentric subdivision $\mathrm{Sd}\dashv\mathrm{Ex}$ set

$$L_n=c_n\mathrm{Sd}^2,\qquad R_n=\mathrm{Ex}^2N_n .$$

Let $W_{KQ}$ and $\mathrm{Fib}_{KQ}$ be the weak homotopy equivalences and Kan fibrations, $I=\{\partial\Delta[m]\hookrightarrow\Delta[m]\}_{m\ge0}$ and $J=\{\Lambda^k[m]\hookrightarrow\Delta[m]\}_{m\ge1}$. Define

$$W_n=R_n^{-1}(W_{KQ}),\qquad F_n=R_n^{-1}(\mathrm{Fib}_{KQ}),\qquad C_n={}^{\perp}(F_n\cap W_n).$$

Formalization targets

Milestone: Equation (7.1), p. 24 — nerve detection

$W_n=N_n^{-1}(W_{KQ})=R_n^{-1}(W_{KQ})$: a functor of strict $n$-categories is a weak equivalence exactly when its Street nerve is a weak homotopy equivalence. This follows from $\mathrm{id}\to\mathrm{Ex}$ being a natural weak equivalence.

Goal: Theorem 1.1 (p. 2)

For every $n\in\{1,2,3,\dots\}\cup\{\infty\}$, $(C_n,W_n,F_n)$ is a proper combinatorial model structure on $n\mathbf{Cat}$, cofibrantly generated by $(L_nI,L_nJ)$, and

$$L_n:\mathbf{sSet}_{KQ}\rightleftarrows(n\mathbf{Cat},C_n,W_n,F_n):R_n$$

is a Quillen equivalence.

Significance

The result itself. The theorem says that strict higher categories, in every dimension, model the homotopy theory of spaces through a genuine model structure, not only after localization. It provides functorial factorizations and lifting on arbitrary strict $n$-categories, including those that are not freely generated, which is what the small-object argument needs. The key new input is a couniversality theorem: pushouts of $c_nN(A)\to c_nN(E)$ along sieves with a right adjoint retraction are Street weak equivalences (Theorem 5.2, p. 18), which is the remaining sufficient condition of Ara–Maltsiniotis.

Formalizing it. Mathlib has simplicial sets and model-category foundations but no strict $\omega$-categories, orientals or Street nerve. A complete development adds these, Steiner's directed complexes, Gray cylinders and local presentability of $n\mathbf{Cat}$, all reusable in higher category theory.

Difficulty

The transfer theorem reduces the model structure to a pushout condition, and that is the hard part: categorical pushouts of strict $n$-categories can create many new composites, so the nerve of a pushout is not the pushout of nerves. Thomason controlled this in dimension 1 with Dwyer maps, but that method does not extend directly. The preprint builds explicit stationary directed prisms (Lemma 3.1, p. 10) that are constant on the old part, so contractions glue across any attachment, and then reduces general posets to finite ones via sieve covers (Corollary 4.5, p. 16; Lemma 4.6, p. 17). Properness (Proposition 7.3, p. 26) and the unit comparison after two subdivisions (Proposition 7.4, p. 27) are separate arguments.

Formalization scope

• OmegaCategory is a structure with a type of cells, source/target maps indexed by ℕ, partial compositions, the globular, unit, associativity and interchange laws, and finite dimension of each cell. Finite $n$ uses a full subcategory NCategory n.
• FullMain asserts: the Kan–Quillen model structure on SSet exists with the standard classes; and, for $\omega$ and every finite $n\ge1$, an ExactModelEndpoint for $L_n\dashv R_n$: a ModelCategory whose weak equivalences, fibrations and cofibrations are exactly $W_n,F_n,C_n$; $(L_nI)^{\pitchfork}=F_n\cap W_n$ and $(L_nJ)^{\pitchfork}=F_n$; both weak factorization systems; completeness, cocompleteness and local presentability; left and right properness; $L_n$ left Quillen; and the Quillen-equivalence criterion at fibrant targets.
• The classes are fixed by equations, so the goal cannot be met by an unrelated model structure.
• The milestone quantifies over every n : ℕ, including $n=0$, which the source does not consider; the identity holds there by the same argument.

Selected references

• OpenAI, Thomason Model Structures in Every Strict Higher Dimension, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Thomason-Model-Structures-in-Every-Strict-Higher-Dimension-September-25-2026/paper.pdf
• R. W. Thomason, Cat as a closed model category, Cahiers Topologie Géom. Différentielle 21 (1980). https://www.numdam.org/item/CTGDC_1980__21_3_305_0/
• R. Street, The algebra of oriented simplexes, J. Pure Appl. Algebra (1987). https://doi.org/10.1016/0022-4049(87)90137-X
• D.-C. Cisinski, La classe des morphismes de Dwyer n'est pas stable par rétractes, Cahiers (1999). https://www.numdam.org/item/CTGDC_1999__40_3_227_0/
• D. Ara, G. Maltsiniotis, Vers une structure de catégorie de modèles à la Thomason sur la catégorie des n-catégories strictes, Adv. Math. (2014). https://doi.org/10.1016/j.aim.2014.03.013
• A. Gagna, Strict n-categories and augmented directed complexes model homotopy types, Adv. Math. (2018). https://doi.org/10.1016/j.aim.2018.04.010
• D. Ara, Théorie de l'homotopie des ∞-catégories strictes, habilitation (2023). https://www.normalesup.org/~ara/files/hdr.pdf
• L. Guetta, G. Maltsiniotis, Homologie polygraphique des systèmes locaux, Adv. Math. (2024). https://doi.org/10.1016/j.aim.2024.109719
• T. M. Fiore, S. Paoli, A Thomason model structure on the category of small n-fold categories, Algebr. Geom. Topol. 10 (2010). https://doi.org/10.2140/agt.2010.10.1933
• P. G. Goerss, J. F. Jardine, Simplicial Homotopy Theory, Birkhäuser (1999). https://doi.org/10.1007/978-3-0348-8707-6

Motivation

A finitely generated group has decidable word problem if an algorithm decides, for every word in a fixed finite generating set and its inverses, whether it represents the identity. Embedding theorems translate this algorithmic property into algebra: Higman (1961) characterized subgroups of finitely presented groups, and Boone and Higman (1974) showed that decidable word problem is equivalent to embedding in a simple subgroup of a finitely presented group, asking whether the simple group can be finitely presented (the Boone–Higman conjecture).

This preprint proves a stronger statement in the direction of higher finiteness: every finitely generated group with decidable word problem embeds in a simple group of type $F_\infty$, i.e. one with a classifying space having finitely many cells in each dimension. Since type $F_\infty$ implies finite presentation, this implies the Boone–Higman conjecture.

Background

• 1961. Higman's embedding theorem: finitely generated subgroups of finitely presented groups are exactly the recursively presented groups.
• 1974. Boone and Higman characterize decidable word problem by embeddings into simple subgroups of finitely presented groups and pose the conjecture.
• 1975, 1987. Brown gives homological criteria for finiteness and establishes type $F_\infty$ for the Thompson–Higman groups.
• 1980. Thompson shows the simple overgroup can be chosen finitely generated with decidable word problem.
• 2022. Belk and Zaremsky introduce twisted Brin–Thompson groups and construct a simple group of type $F_\infty$ containing all finitely generated right-angled Artin groups.
• 2024–2026. Belk, Hyde and Matucci construct a simple $F_\infty$ group containing every countable abelian group; the Boone–Higman conjecture is verified for hyperbolic groups (Belk, Bleak, Matucci, Zaremsky) and for $\mathrm{Aut}(F_n)$ and mapping class groups (Belk, Fournier-Facio, Hyde, Zaremsky). The survey of Belk, Bleak, Matucci and Zaremsky raises the higher-finiteness question.
• 2026. The OpenAI preprint Simple $F_\infty$ overgroups of groups with decidable word problem (dated September 23, 2026) proves the theorem below, building on the companion preprint Finite algebraic envelopes and the Boone–Higman conjecture. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

A classifying space $K(H,1)$ is a connected CW complex with fundamental group $H$ and contractible universal cover. $H$ has type $F_n$ if some $K(H,1)$ has finite $n$-skeleton and type $F_\infty$ if some $K(H,1)$ has finitely many cells in each dimension. Type $F_1$ is finite generation and type $F_2$ is finite presentation. A group is simple if it is nontrivial and has no normal subgroups besides $1$ and itself.

In Lean (OAI.SimpleFInftyOvergroups, definitions SimpleOvergroups), HasDecidableWordProblem G asks for a finite generating tuple with a ComputablePred identity predicate on words; HasTypeFInfty H asks for a Hausdorff connected space $X$ with a CW structure of finite type (Topology.CWComplex.FiniteType), a basepoint with $H \simeq \pi_1(X, x)$, and a surjective covering map from a contractible space.

Formalization targets

Goal: Theorem 1.1

Every finitely generated group $G$ with decidable word problem admits an injective homomorphism $G \hookrightarrow H$ into a nontrivial simple group $H$ of type $F_\infty$.

The input need not be finitely presented and its word-problem algorithm may have arbitrary running time; the classifying space of $H$ may be infinite-dimensional.

Significance

The result. Theorem 1.1 answers the higher-finiteness strengthening of the Boone–Higman conjecture and implies the conjecture itself. With the classical converse (finitely presented simple groups have decidable word problem), it characterizes groups with decidable word problem as the finitely generated subgroups of simple groups of type $F_\infty$.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization requires CW complexes of finite type, classifying spaces and covering theory (partially in Mathlib), Brown's homological finiteness criterion, Steinberg groups, and twisted Brin–Thompson groups with the Belk–Zaremsky finiteness theorem (Theorem 5.1 in the preprint, from the literature).

Difficulty

Finite presentation already fails to pass to subgroups; higher finiteness additionally requires controlling relations among relations in every dimension. Known families of simple $F_\infty$ groups contain large classes of groups but give no general construction from a word-problem algorithm. The proof needs an oligomorphic faithful action of a group of type $F_\infty$ with stabilizers of type $F_\infty$, built from an algebraic envelope whose Steinberg-group kernel must be annihilated exactly (Theorem 4.6).

Formalization scope

• $G$ and $H$ live in the same universe Type u; $G$ carries [Group.FG G].
• IsSimpleGroup H together with Nontrivial H encodes simplicity.
• Type $F_\infty$ is encoded topologically via a finite-type CW structure on a connected Hausdorff space whose universal cover (a surjective covering with contractible total space) witnesses asphericity.
• The word problem uses ComputablePred on lists of (generator, sign) pairs for a specified generating tuple.

The statement is not vacuous: the hypothesis holds for many groups (e.g. all finitely presented residually finite groups), and the conclusion requires a genuine embedding.

Needed infrastructure: finite-type CW complexes and $K(\pi,1)$ spaces, Brown's criterion, group actions with finiteness properties, Steinberg groups over noncommutative algebras, and twisted Brin–Thompson groups. Contributions toward any of these are welcome.

Selected references

• OpenAI, Simple $F_\infty$ overgroups of groups with decidable word problem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Simple-F-infinity-overgroups-of-groups-with-decidable-word-problem-September-23-2026/paper.pdf
• OpenAI, Finite algebraic envelopes and the Boone–Higman conjecture, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/main/preprints/Finite-algebraic-envelopes-and-the-Boone-Higman-conjecture-September-23-2026/paper.pdf
• W. W. Boone, G. Higman, An algebraic characterization of groups with soluble word problem, J. Austral. Math. Soc. 18 (1974). https://doi.org/10.1017/S1446788700019108
• G. Higman, Subgroups of finitely presented groups, Proc. Roy. Soc. London Ser. A 262 (1961). https://doi.org/10.1098/rspa.1961.0132
• R. J. Thompson, Embeddings into finitely generated simple groups which preserve the word problem, in Word Problems II, 1980. https://doi.org/10.1016/S0049-237X(08)71348-X
• K. S. Brown, Homological criteria for finiteness, Comment. Math. Helv. 50 (1975). https://doi.org/10.1007/BF02565740
• K. S. Brown, Finiteness properties of groups, J. Pure Appl. Algebra 44 (1987). https://doi.org/10.1016/0022-4049(87)90015-6
• J. Belk, M. C. B. Zaremsky, Twisted Brin–Thompson groups, Geom. Topol. 26 (2022). https://doi.org/10.2140/gt.2022.26.1189
• J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Progress around the Boone–Higman conjecture, 2025. https://arxiv.org/abs/2306.16356
• J. Belk, C. Bleak, F. Matucci, M. C. B. Zaremsky, Hyperbolic groups satisfy the Boone–Higman conjecture, Duke Math. J. 175 (2026). https://doi.org/10.1215/00127094-2025-0055
• J. Belk, J. Hyde, F. Matucci, Finite germ extensions, 2024. https://arxiv.org/abs/2407.03149

Motivation: algebraic versus geometric dimension of groups

Two numbers measure how "large" a discrete group $\Gamma$ is. The cohomological dimension $\operatorname{cd}\Gamma$ is algebraic: the length of the shortest projective resolution of the trivial module $\mathbb Z$ over the group ring $\mathbb Z[\Gamma]$. The geometric dimension $\operatorname{gd}\Gamma$ is topological: the least dimension of a CW complex with fundamental group $\Gamma$ and contractible universal cover (a classifying space or $K(\Gamma,1)$). Cellular chains of a classifying space give a free resolution, so $\operatorname{cd}\Gamma\le\operatorname{gd}\Gamma$. Eilenberg and Ganea proved in 1957 that equality holds whenever $\operatorname{cd}\Gamma\ge3$, and Stallings and Swan settled dimension one. The remaining case — must a group of cohomological dimension two have a two-dimensional classifying space? — is the Eilenberg–Ganea conjecture, closely tied to Whitehead's asphericity conjecture in low-dimensional topology.

Background

• 1941 — Whitehead asks whether every connected subcomplex of an aspherical 2-complex is aspherical (Ann. of Math. 1941).
• 1957 — Eilenberg and Ganea prove $\operatorname{cd}=\operatorname{gd}$ for $\operatorname{cd}\ge3$ and pose the dimension-two question (Ann. of Math. 1957).
• 1968–1969 — Stallings proves that finitely generated groups of cohomological dimension one are free (Ann. of Math. 1968); Swan removes finite generation (J. Algebra 1969).
• 1997 — Bestvina and Brady introduce height kernels of right-angled Artin groups and show that for suitable flag triangulations of a spine of the Poincaré homology sphere at least one of the Eilenberg–Ganea and Whitehead conjectures fails (Invent. Math. 1997, Thm 8.7).
• 1999 — Dicks and Leary give presentations of these kernels (Proc. AMS 1999); Howie studies them via plus constructions (Math. Proc. Camb. Phil. Soc. 1999).
• 2026 — Leary and Petrosyan compare Coxeter and Bestvina–Brady candidates for the problem (arXiv:2605.07853).
• 2026 — An OpenAI preprint, A finitely generated counterexample to the Eilenberg–Ganea conjecture (OpenAI Math Release, September 23, 2026), claims a finitely generated residually finite group with $\operatorname{cd}=2$ and $\operatorname{gd}=3$. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

For a finite simplicial graph $\Delta$ with vertex set $V$, the right-angled Artin group is

$$A_\Delta=\bigl\langle a_q\ (q\in V)\ \bigm|\ a_qa_ra_q^{-1}a_r^{-1}=1\ \text{whenever } q,r \text{ are adjacent}\bigr\rangle ,$$

and the height homomorphism $\lambda:A_\Delta\to\mathbb Z$ sends every $a_q$ to $1$. Its kernel is a Bestvina–Brady group.

The specific graph comes from the presentation complex $K$ of $\langle x,y\mid x^2y^{-5},\ x^2(yx^{-1})^{3}\rangle$, which is integrally acyclic and has a nontrivial representation of its fundamental group into $\mathrm{SU}(2)$. Subdivide each of the two loops of $K$ into three edges, cone the boundary of each relator polygon to a new interior vertex (keeping one radial edge per boundary occurrence), and take the order complex of the resulting regular cell structure (7 vertices, 51 edges, 45 triangular sectors). This is a flag triangulation $L$ of $K$; $\Delta$ is its 1-skeleton, i.e. the comparability graph of the cells. The group is $G=\ker\lambda\le A_\Delta$.

A group is residually finite if every nontrivial element survives in some finite quotient.

Formalization targets

Goal: the counterexample (Theorem 1.1)

For the group $G$ above,

$$G\ \text{is finitely generated and residually finite},\qquad \operatorname{cd}G=2,\qquad G \text{ has a 3-dimensional } K(G,1),\qquad G \text{ has no 2-dimensional } K(G,1).$$

In particular $\operatorname{gd}G=3\ne2=\operatorname{cd}G$. The non-existence clause holds for classifying spaces with any number of cells. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem disproves the Eilenberg–Ganea conjecture with a finitely generated (indeed type $\mathrm{FL}$, but not finitely presented) residually finite group, so the conjecture fails even for countable groups with strong finiteness properties. By Bestvina–Brady's dichotomy the Whitehead conjecture is not directly decided by this example, but the gap between the algebraic and geometric dimensions in dimension two is now exhibited concretely.

Formalizing it. The statement is concrete: an explicit finite graph, its Artin group and height kernel, a projective dimension, and existence/non-existence of CW models. The non-existence clause ranges over all CW complexes of arbitrary cardinality, which is exactly the kind of universally quantified topological claim where a machine check is valuable. Groundwork includes classifying spaces in Mathlib's CW-complex framework, projective dimension over group rings, and Bestvina–Brady Morse theory.

Difficulty

The kernel acts freely on an acyclic 2-complex, which gives $\operatorname{cd}G\le2$, but an acyclic complex need not be contractible, and showing that one particular 2-dimensional model fails to be a $K(G,1)$ says nothing about other models. The obstacle is to rule out every hypothetical two-dimensional classifying space, with arbitrarily many cells, and to do so for a group that is not finitely presented. Homological invariants cannot see the difference, since they agree with those of a genuine 2-dimensional model.

Formalization scope

• The seed complex is encoded combinatorially: signed relator words seedWord, rose vertices, circle edges and sectors; seedGraph is the comparability graph of the cell face relation. ArtinGroup is a PresentedGroup on commutators of adjacent vertices, height sends each generator to $1$ in Multiplicative ℤ, and SourceGroup is its kernel.
• cohomologicalDimension is the categorical projective dimension (in WithBot ℕ∞) of the trivial $\mathbb Z[G]$-module in ModuleCat.
• HasClassifyingSpace G n asks for a Hausdorff, path-connected CW complex with no cells above dimension $n$, fundamental group isomorphic to $G$, and a surjective covering map from a contractible space. The positive clause is stated in universe 0; the negative clause is universe-polymorphic, so no restriction on the cardinality of cells is imposed.
• Needed infrastructure: Bestvina–Brady level complexes, presentations of height kernels, residual finiteness of RAAG subgroups, $\mathrm{SU}(2)$ representations and degree arguments.

Selected references

• S. Eilenberg and T. Ganea, On the Lusternik–Schnirelmann category of abstract groups, Ann. of Math. 65 (1957). https://doi.org/10.2307/1970062
• J. H. C. Whitehead, On adding relations to homotopy groups, Ann. of Math. 42 (1941). https://doi.org/10.2307/1968907
• J. R. Stallings, On torsion-free groups with infinitely many ends, Ann. of Math. 88 (1968). https://doi.org/10.2307/1970577
• R. G. Swan, Groups of cohomological dimension one, J. Algebra 12 (1969). https://doi.org/10.1016/0021-8693(69)90030-1
• M. Bestvina and N. Brady, Morse theory and finiteness properties of groups, Invent. Math. 129 (1997). https://doi.org/10.1007/s002220050168
• W. Dicks and I. J. Leary, Presentations for subgroups of Artin groups, Proc. Amer. Math. Soc. 127 (1999). https://doi.org/10.1090/S0002-9939-99-04873-X
• J. Howie, Bestvina–Brady groups and the plus construction, Math. Proc. Cambridge Philos. Soc. 127 (1999). https://doi.org/10.1017/S0305004199003928
• I. J. Leary and N. Petrosyan, Universal structure of graph product kernels, preprint, 2026. https://arxiv.org/abs/2605.07853v1
• OpenAI, A finitely generated counterexample to the Eilenberg–Ganea conjecture, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-finitely-generated-counterexample-to-the-Eilenberg-Ganea-conjecture-September-23-2026/paper.pdf