---

Claim. A finite $3$-uniform hypergraph occurs in every $3$-uniform hypergraph of chromatic number $>\aleph_0$ exactly when, after its isolated vertices are deleted, it is linear, every edge-node of its Levi graph meets a bridge, and every Berge cycle has even length. This is the characterization that Problem 593 asks for, and the same answer that Li's preprint gives. The manuscript is Samuil Petkov's paper titled, in print, Obligatory Triple Systems: An Alternative Proof (the README of its repository, SamPetkov/Erdos593, calls it Obligatory Triple Systems: Alternative Proof and Lean Verification; manuscript revision of 2026-07-21 per that README; the links above are pinned to the repository's commit of 2026-10-04).

Submission note. Posted to erdosproblems.com as a proof claim by Samuil Petkov (account Sam_Petkov) on 15 July 2026, giving "5.6 Sol Pro" as the AI used:

We characterize exactly which finite triple systems must occur in every uncountably chromatic triple system: after deleting isolated vertices, they are precisely the linear systems in which every hyperedge-node meets a bridge in the Levi graph and every Berge cycle has even length. The proof first forces private-vertex expansions of finite bipartite graphs using codegrees, closure chains, and a rainbow bipartite argument; then proves closure under disjoint unions and one-point amalgamations via rooted-copy abundance; next cuts the Levi graph along bridges to recover the constructive decomposition; finally it builds explicit uncountably chromatic avoiding hosts when linearity, the bridge condition, or parity fails. The new ingredients are the direct expansion argument, the rooted-abundance lemma, and the finite-trace analysis of sequence lifts, all carried out in ZFC. Notes: Proof completed with ChatGPT-5.6 Sol Pro, verified independently by Pro 2 times and Ultra 2 times. Formalisation underway. Not verified by an expert!

Argument, in outline. The manuscript proves the forcing direction first: a rainbow lemma, proved probabilistically, supplies the injectivity needed to force the private-vertex expansion of every finite bipartite graph, and a lemma on the abundance of rooted copies gives closure under one-point amalgamation, singular uncountable cardinals included. To pass from the Levi-graph criterion to the generated class it removes chosen bridges of the Levi graph, identifies each remaining component with such an expansion, and recovers the amalgamation order from the tree structure of the quotient. For the avoidance direction it adopts the sequence-lift and bridge-trace method of Li's preprint, with the trace statement reproved through a decomposition of the lift into a base and fibers joined only at cut points, so that a missing bridge or an odd Berge cycle cannot be assembled across fibers; the three obstructions are then met by three hosts, a linear host from the Erdős–Rado partition theorem for nonlinearity, the lift of $K_{\omega_1}$ for a hyperedge-node with no bridge, and an Erdős–Hajnal graph of uncountable chromatic number and prescribed odd girth for an odd Berge cycle. Everything is in ZFC, with the de Bruijn–Erdős compactness theorem as the third imported input.

Standing. The claimant is Samuil Petkov, who filed the result on the site's proof-claims page on 2026-07-15 under the forum name Sam_Petkov; the claim's entry names the system 5.6 Sol Pro and its notes say that the proof was completed with ChatGPT-5.6 Sol Pro, verified independently twice by Pro and twice by Ultra, as the notes name the two checkers, and not by an expert; the manuscript itself names GPT-5.6 Pro through ChatGPT and Aristotle for proof development, checking and the Lean formalization. The manuscript states that Theorem A, its classification, was first proved by Li, credits Li's preprint of 2026-06-23 as the first publicly posted complete proof, makes no priority claim for the ingredients it reuses, and claims no informational independence: the author began the argument before learning of Li's preprint, but the instruction that the models work without further internet access after an initial source-retrieval stage is, as the manuscript says, no auditable guarantee that no model suggestion drew on outside retrieval; it presents itself as an alternative proof whose main expository difference is a base-fiber decomposition suited to machine checking. The manuscript and the repository's README describe a Lean 4 formalization whose exported theorems are the two equivalences F.IsObligatory ↔ F.isolatedReduction.Intrinsic and F.IsObligatory ↔ Constructible F.isolatedReduction; the claimant states that the development verifies both directions of the classification including the isolated-vertex reduction, that the word finite refers to the classified system $F$ while the host triple systems are not assumed finite and are quantified within the formalization's documented ambient-universe convention, and that the Lean is a separate verification of the alternative proof, not a line-by-line formalization of Li's manuscript. The entry file formalization/Erdos593.lean calls itself the entry point of a machine-checked finite structural kernel and imports the graph and triple-system modules. This corpus has not built or audited the development or compared its definition of an obligatory system with the uncountably chromatic hosts of the question, so the page lists no formalized evidence. The site lists seven comments on the claim. On 2026-07-15 a commenter pointed to Li's arXiv preprint, and the claimant replied that Li's preprint claims the same classification by a different and in some respects stronger route, that Pro and Ultra had found no fatal gap in it though they could not certify it themselves, and that their own proof was narrower, independent and more self-contained in the ingredients Problem 593 needs. On 2026-07-17 Li noted that the preprint had been public since 2026-06-23 and could have been retrieved by a system producing a later proof, and invited collaboration on formalizing it; the claimant answered that they had been unaware of Li's work, that the important arguments differ and Li's proof is more elegant and stronger, and that the first parts of the two proofs are the same. On 2026-07-19 the claimant announced the formalization complete and checked by Aristotle, ChatGPT and the repository's continuous integration build. On 2026-07-20 Li reported that at the revision of 2026-07-19 the development compiled under its pinned toolchain and that #print axioms on both endpoint theorems gave only propext, Classical.choice and Quot.sound, a third party's report that is not corpus evidence, and proposed a timeline crediting Li's preprint with the first resolution and this development with the first machine-checked proof of the classification; the claimant replied that the claim stays up for historical purposes, since Li's claim was first. So the claimant asserted independence in their comment of 2026-07-15, and the manuscript revision of 2026-07-21 later disclaimed informational independence while keeping the alternative route. The site shows no verdict and its label is OPEN; the manuscript is not refereed and no reviewer is recorded, so the claim stays claimed.