#593 and #1177: Eric Li's obligatory-triple-system classification, independently rebuilt from scratch

Not a discovery — targeted scrutiny of an existing, already-flagged claim. Both erdosproblems.com/593 (a $500-prize problem) and #1177 already show a comment (Alfaiz, 24 Jun) noting Eric Li's paper claims to resolve them. On #1177's page, Nat Sothanaphan adds a specific, fair caution: Li is a "3rd year CS undergraduate" who has "claimed to solve multiple problems on this site in a row, with non-short papers" — not a reason to dismiss the work, but a reason it deserves more scrutiny than usual before anyone trusts it. Nobody in either thread had done a full independent rebuild. That's what we did.

The problems. #593: characterize which finite 3-uniform hypergraphs must appear in every 3-uniform hypergraph of chromatic number >ℵ₀. #1177: three exact-cardinal questions about the avoidance classes F_G(κ) (does nonemptiness at ℵ₁ give a bounded-size witness; can two nonempty avoidance classes fail to share a member; does nonemptiness at one uncountable cardinal give nonemptiness at every uncountable cardinal). Li's paper (arXiv:2606.24882) answers all of it — the classification for #593, and yes/no/yes for #1177's three parts — as a single unconditional theorem with zero hypotheses.

What we actually did. Cloned Li's repo (github.com/ericlisg/erdos-593-1177-lean) on a disposable box, built the entire ~8,000-job project from source against pinned Mathlib, then ran #print axioms on every individual component (the Erdős–Hajnal odd-girth case, EGH, Reiher, the HK loose-7 case, all three parts of #1177) and the master theorem:

'Erdos593.full_resolution_unconditional' depends on axioms:
[propext, Classical.choice, Quot.sound]

Every single one clean — no sorryAx, just the standard three. The repo's own build pipeline runs this same audit automatically; we didn't take that on faith either, we reproduced the whole thing ourselves, from a clean clone, on infrastructure we controlled.

What this doesn't settle. A clean Lean kernel check confirms the formalized statement is proved — it doesn't confirm the formalization faithfully captures the informal problem (a live concern named in Nat's own comment, and the right next scrutiny step: read the Lean statement against the tracker's exact wording line by line, which we haven't done as carefully as we did the axiom check). And "no human has read this end to end" was Woett's fair caution on the sibling #768 case — the same applies here.