A greedy matching is a matching produced by processing the edges of a graph in an order and accepting each graph edge whose vertices are both unmatched. The result is a maximal independent edge set, but need not be a maximum independent edge set. In a bipartite graph describing jobs and bins, a related greedy algorithm processes jobs in arrival order and assigns each job to an available neighboring bin. If each bin can accept several jobs, its capacity limits the number of assignments it receives rather than requiring every graph vertex to occur in at most one accepted graph edge.
Arnosti (2022) studied a random bipartite graph in which each job independently chooses a uniformly distributed subset
of the bins of a prescribed size. Every bin has the same positive integer
capacity 
.
RANDOM-VERTEX chooses a uniformly random available neighboring bin, whereas RANKING
chooses the available neighboring bin with highest priority in one shared random
ordering of the bins. Job arrival order and bin priority order are independent of
the chosen neighborhoods. Arnosti (2022) proved equality of the resulting statistical
distributions for 
and stochastic dominance of RANDOM-VERTEX
for 
,
and conjectured the latter for 
.
MathIsEvenEasier (2026) reported the comparison
 |
where 
denotes the number of assigned jobs, for every common capacity 
and every integer threshold
. GPT-6 Astra developed the argument
and Lean formalization under human direction. As of Oct. 7, 2026, a public continuous-integration
run had compiled all 91 positive modules, rejected a deliberately false control,
and reported only standard Lean axioms for the final theorem (VibeMathed 2026). Independent
specialist review had not been reported. The comparison averages over the random
neighborhoods; it does not assert an inequality on every run or for an arbitrary
fixed bipartite graph, and unequal bin capacities
are outside its scope.
