Sparse coloring for isosceles-free grids: an AI-assisted proof case study

We study the largest size $C(n)$ of a subset of the $n\times n$ integer grid containing no isosceles triple, including equally spaced collinear triples. We prove $C(n)=\Omega\left(n\sqrt{\log\log n/\log n}\right)$ by applying the sparse hypergraph coloring theorem of Cooper and Mubayi. Elementary geometry and primitive-direction counts give maximum degree $O(n^2\log n)$ and pair-codegree at most $5n$ for the forbidden-triple hypergraph. The resulting bound improves the explicit guarantee in PatternBoost by a factor of order $\sqrt{\log\log n}$. Recovered interaction records document how a Codex literature proposal, human route selection, finite verification, and author-relayed review informed proof synthesis and repair. We connect these actions to successive proof artifacts and extract two case-derived checking practices: tracking objects, parameters and conclusions in theorem applications, and seeding a definitional omission to test a finite verifier. Separately implemented enumerators agree on complete edge sets for every $2\le n\le12$; suppressing the degenerate-case branch loses exactly the equally spaced collinear triples. These records document assistance under human direction, and finite checks support implementation consistency rather than the asymptotic theorem itself.