The teorth/erdosproblems repository (the community database behind erdosproblems.com and the source catalog for FrontierMath Erdős) carries data/problems.yaml: 1,221 problems, 593 marked open, tagged across 43 distinct subject tags. erdos_catalog_crosscheck.py matched a keyword fingerprint of this corpus's actual proven machinery against every tag and against the full text of the catalog's own README index:
Not one of the twenty-odd terms above appears in any of the 43 tags, and not one appears anywhere in the catalog's 457 KB README index. The 43 tags actually present are: additive basis, additive combinatorics, algebra, analysis, arithmetic progressions, base representations, binomial coefficients, chromatic number, combinatorics, complete sequences, convex, covering systems, cycles, diophantine approximation, discrepancy, distances, distribution, divisors, factorials, geometry, graph theory, group theory, hypergraphs, intersecting family, irrational, irrationality, iterated functions, number theory, planar graphs, polynomials, powerful, powers, primes, primitive sets, probability, ramsey, ramsey theory, set theory, sidon sets, squares, topology, turan number, unit fractions.
Two near-misses were checked by hand rather than left as tag noise. covering systems (22 open problems) sounds adjacent to Coverage.lean's hex-ring coordinate-injectivity theorem, until the actual problems are read: they are modular arithmetic — covering the integers by residue classes, e.g. problem 274, the Herzog–Schönheim conjecture on coset covers of a group. Unrelated to a spatial coverage argument beyond the English word. geometry + distances (108 and 55 tagged problems respectively, many open) is Erdős's own distinct-distances and unit-distance territory — genuinely about points in the plane, and the closest thing in the catalog to HexForm.lean's subject. No problem statement or tag mentions the hexagonal or triangular lattice, the Eisenstein integers, or the specific quadratic form Q(q,r) = q²+qr+r² that file is actually about.
A corpus that only reports the threads that worked is not reporting its actual hit rate. This one check took under a minute to run once the fingerprint was written and cost nothing to be honest about: Paul Erdős's own problems concentrate overwhelmingly in number theory, graph theory, Ramsey theory and additive combinatorics — the combinatorics of integers and finite structures. This corpus's proven machinery sits in discrete differential geometry and low-dimensional dynamical systems — a genuinely different neighbourhood of mathematics, not a thread waiting to be noticed. That does not make this corpus's open-problem threads worthless; it means the Erdős catalog specifically is not the map for them. §1's Skolem Problem thread came from a different source (Tao's own open-question list and the FrontierMath sample problems) for exactly this reason, and it is not filed here as an Erdős problem, because it is not one.