A computer-assisted proof of the four-uniform Erdős matching conjecture

We prove the Erdős matching conjecture for four-uniform hypergraphs for every matching parameter and every admissible number of vertices. The proof combines the finite-board method of Hou, Hu and Liu with ordered local configurations, exact integer counts and certified inequalities. Small matching parameters are treated on full labelled configurations. Two fixed counting inequalities and two endpoint anchors propagate polynomially across the remaining range; 51 endpoint records and the two fixed inequalities suffice for the intermediate cardinality inputs. Dense triple supports admit direct slab and majority proofs. A classical shadow bound and a deletion argument complete the passage from these local bounds to the global theorem. The strict margins also yield clique stability with explicit constants for shifted families whose matching number is preserved on deleting the first vertex, and classifications of extremizers in specified ranges. The finite parts are supported by exact certificates and exhaustive computations with stated mathematical specifications.