265 missions · 158 completed
The mathematics of finite and discrete structures — counting the arrangements of a set, deciding when a configuration meeting prescribed constraints can exist, and characterizing the patterns such structures are forced to contain. It encompasses enumerative and extremal combinatorics, graph theory, design theory, and additive combinatorics, with deep ties to algebra, probability, and computer science.
This mission formalizes the lower bound on the number of reversible binary cellular automata on the Moore neighborhood. Extending the conserved-landscape marker families to both centered and off-centered rules.
A convex polytope has both geometric coordinates and a finite pattern of faces. Moving its vertices can change distances and angles while preserving which vertices belong to which faces. Enumeration by combinatorial type asks for those incidence patterns, with geometrically different realizations of the same pattern counted together. Grünbaum’s enumeration theorem establishes that the complete collection can be determined algorithmically when the dimension and number of vertices are prescribed Convex Polytopes, §5.5, p.91.
A d-polytope here is a nonempty convex hull of finitely many points in real d-dimensional coordinate space, with affine span equal to the whole space. A face is obtained by maximizing a linear functional over the polytope; the collection of faces also includes the empty face and the polytope itself. Inclusion orders this collection. Two polytopes have the same combinatorial type when their full face collections admit an order isomorphism. This notion retains the incidence structure and forgets metric measurements.
To describe a type with finite data, label the k vertices by the integers from zero through k−1. Record the set of vertex labels belonging to each nonempty proper face. This family of subsets is the polytope’s scheme. A finite list of finite lists of natural numbers encodes such a family. The order of labels and repeated occurrences of a label do not change the represented subset. A scheme is realized only when its recorded subsets are exactly the vertex sets of the nonempty proper faces: it cannot add faces, omit faces, or introduce labels outside the prescribed range.
The target is a single total computable function
For every dimension d and vertex count k, each scheme in E(d,k) must have a realizing d-polytope with exactly k vertices. Every d-polytope with k vertices must realize some scheme in that output. Finally, if polytopes realizing two output positions have isomorphic full face posets, those positions must be equal. These requirements say that the output contains precisely one representative of every combinatorial type. The existential choice of one function precedes both numerical inputs, so the algorithm must work uniformly for all dimensions and vertex counts.
The result supplies an effective finite classification at each prescribed size. It is stronger than the observation that only finitely many incidence families can be written down: those families need not all arise from real convex polytopes. It also addresses termination, since a total algorithm must return its entire finite answer for every input. The theorem is a known mathematical result in the cited textbook. The present formal target asks for a proof of its stated algorithmic conclusion; no machine-checked proof of that conclusion is asserted here.
The principal difficulty is the connection between finite incidence data and geometric realizability. Combinatorial consistency alone does not supply real coordinates for a convex polytope. The source distinguishes this realizability question from the enumeration conclusion and identifies decidability over the real numbers as relevant to it §5.5, p.91. The mission retains the complete enumeration conclusion, including realizability of each answer, coverage of every type, and absence of duplicate types.
The formal representation uses real coordinates without a rationality restriction and permits nonsimplicial polytopes. Vertices are labelled injectively and exhaustively. The number of vertices is expressed as the number of nonempty zero-dimensional exposed faces. Nonemptiness separates the empty face, whose book dimension is −1, from the natural-valued dimension used to count faces. For finite convex hulls the face collections are finite, so this cardinality has its usual meaning.
Natural-number dimensions include dimension zero. The unique point has one vertex and no nonempty proper faces, and therefore uses an empty scheme. This is an explicit extension of the source’s positive-dimensional scheme convention. Unrealizable dimension and vertex-count pairs require an empty output. Finite-polytope faces, their ordered collection, vertex counts, and finite scheme realizations are the concrete objects needed to state the goal; total computability applies to the complete finite output rather than to individual tests alone.
Reference: Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.5, Theorem 2 (5.5.2), printed p.91, PDF p.117; definitions in §§2.4 and 3.1. Source text.
A vector whose coordinates are all zero or one records a collection of yes-or-no choices. Taking the convex hull of a collection of these vectors gives a 0/1-polytope, also called a binary polytope. Such objects connect discrete choices with geometry: points describe feasible combinations, while supporting inequalities describe restrictions that every feasible combination satisfies. Grünbaum's discussion in §4.9 emphasizes the role of facets of these polytopes in combinatorial optimization and cutting-plane descriptions.
The question here concerns how many facets can occur when the dimension grows. Restricting every generating point to binary coordinates gives a finite, highly structured collection of possible points. Nevertheless, this restriction still allows polytopes with very many distinct boundary faces. The theorem of Bárány and Pór establishes superexponential growth in the largest possible number of facets. The mission concerns the form of this growth asserted in Grünbaum's 2003 notes, printed page 69a, rather than a prescribed numerical constant.
Fix a natural number d. The ambient space is the real coordinate space R^d. A convex hull consists of all convex combinations of the generating points, meaning weighted averages with nonnegative weights whose sum is one. A polytope is the convex hull of a finite set of points. It is full-dimensional when its affine span is all of R^d; this rules out a polytope lying in a proper affine subspace.
For a binary polytope, every generating point belongs to {0,1}^d. A subset of this cube is automatically finite. Nonemptiness and full dimension are imposed separately in the target. Consequently, the dimension in the facet bound is the actual dimension of the polytope as well as the dimension of its coordinate space.
An exposed face is the set of all points of the polytope that maximize a given linear functional. A facet is a face of affine dimension d−1. Facets are counted as geometric sets. Two different inequalities that expose the same face do not contribute two facets. Write f_(d−1)(P) for this number.
The target is the following existence statement:
The constant c and threshold D are chosen before the dimension d. The polytope P may depend on d. The assertion therefore supplies a witness in every sufficiently large dimension. It does not merely assert the existence of one complicated polytope or of witnesses along an unspecified subsequence.
The logarithm is natural. Replacing it by another fixed base greater than one changes the admissible constant c, while preserving the shape of the theorem. The statement leaves both c and D unspecified. The Bárány–Pór paper, Theorem 1.1, supplies the asymptotic context for the book's formulation.
For any fixed c greater than one, the expression c^(d ln d) eventually exceeds A^d for every fixed A greater than one. Thus a single exponential base cannot bound the facet counts of all binary polytopes across dimensions. The binary-coordinate restriction alone does not yield that kind of uniform bound.
The underlying mathematical result is established in the literature. The formalization task is to prove its stated existence conclusion with the precise geometric definitions above. The conclusion concerns actual facets of actual polytopes, so a family of redundant inequalities or a list with repetitions would not satisfy the counting requirement.
A large supply of binary points does not by itself identify the supporting hyperplanes of their convex hull. Counting points and counting facets are different tasks. Moreover, the theorem requires the same growth constant across all sufficiently large dimensions. Verifying individual examples, even examples with many facets, leaves that uniform asymptotic requirement unresolved.
The book describes certain random polytopes as witnesses. Its stated conclusion gives no probability distribution or numerical probability bound. The target records the resulting extremal existence assertion; it imposes no extra probabilistic hypothesis on the witness.
The coordinate model is Fin d → ℝ. IsDPolytope requires a nonempty finite convex hull with full affine span. IsZeroOnePolytope specifies the hull of binary-coordinate points. faceCount P k counts nonempty exposed faces with affine dimension k. These concrete notions also apply to other questions about finite-dimensional polytopes.
Face counts use natural cardinality. On the domain of finite polytopes there are only finitely many faces, so this is the ordinary finite count. Requiring D at least two ensures that d−1 represents the facet dimension without a low-dimensional subtraction convention and that the logarithm's argument is positive. Full dimension excludes the whole polytope from the facet count, and nonemptiness excludes the empty face.
A convex set can be studied through its images in spaces of smaller dimension. Each image records part of the geometry, while losing the information along the directions that are collapsed. A finite convex hull always has finite convex hulls as its affine images. The converse asks whether sufficiently rich projection data can force the original set to have a finite description by points. This mission concerns the recognition theorem attributed to Klee in Grünbaum's Convex Polytopes, §5.1, Theorem 8, printed page 74.
The question concerns all projections into a suitable dimension, rather than an individual view of a set. A single image may conceal directions in which the original set has additional structure. The theorem identifies a condition on the entire family of images that characterizes polytopes among bounded convex sets.
Fix an integer . Real coordinate space consists of vectors with real coordinates. A set is convex if it contains the line segment joining any two of its points. It is bounded if its points remain within some finite distance of the origin. Neither condition requires to fill the ambient space.
The convex hull of a set , written , is the smallest convex set containing . A polytope is the convex hull of a finite set. The generating set need not be a minimal set of vertices. Grünbaum gives this characterization in §3.1, printed page 31. The empty generating set is permitted, as are generating sets contained in a proper affine subspace.
An affine map preserves affine combinations. A surjective affine map has a -dimensional target and reaches every point of that target. When , such a map loses dimensions. This represents the singular affine images called projections in §5.1, printed page 71, with coordinates chosen on the target affine space. Translation of the target is allowed.
For every bounded convex set , the goal is the equivalence
The dimension may depend on , but it is chosen before testing the affine maps. Every surjective affine map with that target dimension is tested. For each such map, the finite set generating the image can be different. No common set of projected vertices or uniform bound on the number of generators is required.
This is one recognition theorem, containing both implications. The selected source grouping does not introduce separate supporting theorem targets.
The theorem characterizes a global finite convex-hull property through lower-dimensional images. In particular, the conclusion concerns the original set itself; it does not merely assert that its closure has a finite generating set. This distinction matters because boundedness and convexity alone do not assert closedness.
The result is a known mathematical theorem in the source. The formalization target is its complete equivalence with the stated domain and quantifier order. A proof of only the preservation of polytopes under affine maps would leave the recognition implication unresolved.
Every tested image can have its own finite generating set. Finiteness of each image does not directly supply a finite generating set that works in the original ambient space. The recognition implication must connect the universal family of images to the geometry of the whole set. Replacing that family by a convenient fixed projection would change the question.
Real -space is represented by functions from Fin d to the real numbers. Boundedness and convexity use the ordinary Mathlib predicates, and being a polytope is expressed directly by existence of a finite set with the specified convex hull. No full-dimensional polytope structure is imposed on .
The hypothesis makes explicit the admissible ambient dimension needed for . In dimension three, the only available target dimension is two. No assertion of the displayed existential criterion is made in dimensions zero, one, or two. Empty sets, singleton sets, and other lower-dimensional subsets remain within the domain in every admissible ambient dimension.
Affine maps are required to be surjective onto the selected coordinate space. Thus their rank is exactly the selected target dimension, rather than an accidentally smaller rank. Closedness, nonemptiness, rational coordinates, and a predetermined number of vertices are not additional hypotheses. The mathematical ingredients are real convex hulls, finite sets, bounded sets, and affine images.
Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003. Theorem 5.1.8, printed page 74 (source.pdf page 100); projection convention, printed page 71 (PDF97); polytope convention, printed page 31 (PDF51). The source pages are included in this package's evidence directory.
A polytope can be represented by cutting a higher-dimensional simplex with an affine flat. The geometry of the cut determines the resulting polytope. Perles's prescribed-point theorem adds a constraint to this representation: the cutting flat must pass through a point chosen in advance inside the simplex. Theorem 5.1.10 in Branko Grünbaum's Convex Polytopes, second edition (2003), shows that this requirement can always be met when the simplex has enough facets. The source is §5.1, printed page 74, with the section convention introduced on printed page 71.
A polytope is the convex hull of finitely many points. In this mission it is nonempty and full-dimensional in its ambient real coordinate space. Thus a d-polytope P in R^d contains enough points to span that space affinely. A face is the set of points on which a supporting linear functional attains its maximum; a facet is a face of dimension d−1. Different supporting functionals can describe the same face, so the facet allowance counts geometric faces rather than inequalities used to describe them.
A k-simplex is the convex hull of k+1 affinely independent points. Write its vertices as v₀,…,vₖ in R^k and its convex hull as T. Affine independence means there is no nontrivial affine relation among these vertices. The simplex therefore has dimension k, and its interior is taken in the whole space R^k. No restriction is placed on its side lengths or angles. A d-flat is a translate of a d-dimensional linear subspace. A section of T by such a flat L is the entire intersection T ∩ L.
The target is the following existence assertion. For every d-polytope P with at most k+1 facets, every k-simplex T in R^k, and every p in the interior of T, there is a d-flat L such that
An affine equivalence here preserves affine combinations and is invertible on the affine spans. It can change lengths and angles. In the stated coordinates, it is represented by an injective real affine map A from R^d onto L satisfying
All input data, including the interior point p, are universally quantified before the flat and map are chosen. The flat can depend on these data. The source writes the facet allowance as f and the simplex dimension as f−1; the notation here uses f=k+1.
The prescribed-point conclusion gives control beyond the existence of some simplex section representing P. It permits the simplex and an interior point to be fixed while the cutting flat is selected to recover the given polytope. The conclusion concerns its full affine geometry: the image of every point of P lies in the section, and every point of the section belongs to that image. This is the additional representational constraint discussed immediately before Theorem 10 on printed page 74.
The difficulty lies in meeting these requirements simultaneously. A flat through the chosen point can have an intersection of the wrong affine shape. A section with the correct affine shape need not contain the prescribed point. The theorem requires both properties for every allowed simplex and point, while retaining the original facet bound. Neither a special regular simplex nor a selected interior point captures this quantifier structure.
The formal statement uses real coordinate spaces indexed by finite sets, finite convex hulls, affine spans, exposed faces, and affine maps. Nonempty faces are counted by their affine dimension. In dimension zero the facet allowance is automatic: under the convention counting the empty face it contributes at most one facet, which fits the allowance k+1. This avoids interpreting natural subtraction d−1 as a facet dimension at d=0. The zero-dimensional simplex and zero-dimensional polytope remain within the statement.
This is a known geometric theorem whose formal proof remains to be supplied. The target contains one proof placeholder. The definitions specify the underlying geometry concretely. The mission consists of the single prescribed-section theorem; its definitions support that statement, and no separate supporting theorem is included as a milestone. The source is Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.1, Theorem 10, printed page 74 (source.pdf page 100); see also §5.1, printed page 71 (PDF page 97), for the section convention.
A convex polytope has geometric coordinates and a combinatorial structure: its faces, ordered by inclusion. Different coordinates can describe the same combinatorial type. Gale transforms connect these viewpoints by encoding affine dependencies among the vertices as another point configuration, often in a smaller-dimensional space.
Let P and Q be full-dimensional d-polytopes in real coordinate space, each with n vertices. Choose injective lists V and W containing all their vertices and fix a permutation θ of the n indices. The question is whether this prescribed vertex correspondence extends to an isomorphism between the full face posets of P and Q. The empty face and the whole polytope are included in these posets.
An affine dependency of V is a list of real coefficients a whose sum is zero and whose weighted sum of the vertices is zero. These coefficient lists form a vector space of dimension n−d−1. Choose any basis and put its vectors into the columns of a matrix. The n rows of this matrix form a Gale transform G of V. A Gale transform H of W is constructed in the same way, with its own choice of basis. The rows may repeat and may be zero; there is no general-position assumption.
Theorem 5.4.5 states that the prescribed correspondence extends to an isomorphism of face posets exactly when it preserves every relative-interior test on the Gale configurations. For every subset J of vertex indices, the origin belongs to the relative interior of the convex hull of the rows G(J) if and only if it belongs to the relative interior of the convex hull of H(θ(J)). Relative interior means interior within the affine span of the selected convex hull, not interior in the whole coordinate space.
The equivalence concerns every subset of indices and both directions of implication. It retains the prescribed permutation rather than merely asking whether the polytopes have some combinatorial equivalence. Indexing the Gale points also keeps track of which original vertices they represent when several Gale rows coincide. Taking a set image does not change the convex hull of a chosen subconfiguration.
The empty subset is included: its convex hull has empty relative interior, so both membership tests are false. For a simplex, n=d+1 and the Gale space has dimension zero. Its nonempty row subconfigurations consist of the zero vector, and the relative-interior formulation still applies. Zero-dimensional polytopes are also retained.
This mission is the equivalence criterion itself, with the concrete definitions of a full-dimensional polytope, its face poset, and a Gale transform. The grouping keeps transform construction within the vocabulary of the criterion. The neighboring results on affine and projective equivalence have different conclusions and are outside this goal.
Source: Branko Grünbaum, Convex Polytopes, second edition (2003), §5.4, Theorem 5, printed page 89 (PDF page 115). The affine-dependence construction appears on printed pages 85–86 (PDF pages 111–112).
Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.
The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly candidate_only: it is bounded search evidence, not a proof of the unrestricted theorem.
A tournament is an orientation of a finite complete simple graph. For each pair of distinct vertices , exactly one of and is present. Every directed arc receives one of three labeled colors.
A rainbow directed triangle is a cyclically oriented triangle
whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.
A vertex is a monochromatic source when, for every vertex , there is some color and a directed -to- path all of whose arcs have color . The chosen color may depend on ; the theorem does not demand one common color for all targets. Length-zero reachability handles .
The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.
For every nonempty finite tournament with a three-coloring of its arcs,
No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.
The first milestone freezes the exact bounded claim supported by the replay package:
The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.
The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.
The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc may encode that cannot reach ; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.
The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.
The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.
Lean represents the tournament as a binary relation D with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.
The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.