Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Statement
For every integer , there is a finite -uniform hypergraph without property B and a map such that for every edge and every vertex has at most two preimages. Consequently,
for every vertex set .
Source. KoishiChan, Erdős Problems forum comment, 4 December 2025; source and acceptance record.
Rewritten proof
Let be a set of vertices. For every ordered pair of -element subsets of , introduce a new vertex and the two edges
Let be the set of all the vertices . For every -element set and every -element set , introduce a new vertex and the two edges
These are all the edges of . Each has vertices.
Suppose that a red-blue coloring has no monochromatic edge. If contains at least red vertices and at least blue vertices, choose a red -set and a blue -set . If is red, then is red; if it is blue, then is blue. Both alternatives are impossible.
Thus one color occurs fewer than times in . The other color, say red, occurs at least times. Choose a red set of size . For every ordered partition into two -sets, must be blue, since it completes each red set and to an edge. There are distinct such vertices, so choose a blue -set .
Choose any red -set . The edge forces to be blue, while the edge forces it to be red. This contradiction proves that has no property B.
For the counting assertion, map both edges associated with to that vertex, and map both edges associated with to that vertex. Each edge is mapped to one of its own vertices, and no vertex receives more than two edges. If , then ; hence all edges contained in belong to , whose size is at most .
Consequence for Problem 1022
If and is nonempty, then
The hypergraph therefore satisfies the hypothesis with this but is not two-colorable. If constants with the proposed property tended to infinity, some would have , giving a contradiction.
This differs from Wood's construction. The present proof uses an explicit two-level forcing gadget and a two-to-one edge assignment; Wood constructs triangle-free degenerate hypergraphs by induction and obtains the stronger strict bound for every valid constant.
Formalization
The plby/lean-proofs development formalizes this construction and proves the negation of the proposed existential statement. The repository credits KoishiChan as informal author and Aristotle and Boris Alexeev as formal authors. The source was inspected for this compilation, but the Lean project was not built here.