A Resolution of Erdős Problems 593 and 1177: Obligatory Triple Systems and Exact Spectra
Eric Li
math.CO
Jun 23, 2026 · v2
TL;DR
All results, including the resolutions of Erdős Problems 593 and 1177, are formalized in Lean 4 over Mathlib, developed with Aristotle (Harmonic).
Abstract
We resolve Erdős Problems #593 and #1177. Problem #593 asks which finite triple systems occur in every uncountably chromatic triple system; the answer is exactly the class generated from private-vertex expansions of finite bipartite graphs by finite disjoint unions and one-point amalgamations. Equivalently, after isolated vertices are removed, a finite triple system is obligatory precisely when it is linear, every hyperedge-node of its Levi graph has an incident bridge, and every Berge cycle is even. The proof uses an exact bridge-trace theorem for complete-rank one-apex sequence lifts. We also prove that, for every uncountable cardinal kappa, there is a linear triple system of chromatic number exactly kappa, with at most 2^{2^mu} vertices when kappa=mu^+. These two ingredients give a class-valued exact avoidance-spectrum dichotomy for every finite forbidden triple system. As a consequence, Erdős Problem #1177 has truth values yes, no, and yes. All results of this paper have been formally verified in Lean-4.
Problem
Erdős Problem #593 asks which finite triple systems occur in every uncountably chromatic triple system. Erdős Problem #1177 asks three questions about exact avoidance spectra of finite forbidden triple systems.
Approach
Obligatory triple systems are classified via an exact bridge-trace theorem for complete-rank one-apex sequence lifts, together with a running-intersection decomposition into private-vertex expansions of bipartite graphs. A separate exact linear calibration builds, for every uncountable cardinal kappa, a linear triple system of chromatic number exactly kappa, using the Erdős–Galvin–Hajnal labelling property. The results are formalized in Lean 4 (v4.28.0) over Mathlib, with a public GitHub repository developed with Aristotle.
Results
A finite triple system is obligatory exactly when it lies in the class generated by bipartite expansions, equivalently when it is linear, bridge-incident and Berge-even. Exact spectra are either empty or all uncountable cardinals, so Problem #1177 has answers yes, no, yes. The combined Lean theorem depends only on the standard axioms propext, Classical.choice and Quot.sound.
