Sparse coloring for isosceles-free grids: an AI-assisted proof case study
Abstract
We study the largest size C(n) of a subset of the n× n integer grid containing no isosceles triple, including equally spaced collinear triples. We prove C(n)=Ω(n√(loglog n/log n)) by applying the sparse hypergraph coloring theorem of Cooper and Mubayi. Elementary geometry and primitive-direction counts give maximum degree O(n2log 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 √(loglog 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≤ n≤12; 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.
Related
- Strong coloring numbers of grids
- Coloring sparse random Cayley graphs
- Higher-order finite element de Rham complexes on sparse grids
- Anisotropic Kernel-based Multilevel Interpolation of High-Dimensional Functions on Sparse Grids
- List coloring C3-free planar graphs with a sparse matching of restricted lists
BibTeX
@misc{song2026sparse,
title = {{Sparse coloring for isosceles-free grids: an AI-assisted proof case study}},
author = {Yukai Song},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.04194},
eprint = {2610.04194},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.04194},
}
RIS
TY - UNPB
TI - Sparse coloring for isosceles-free grids: an AI-assisted proof case study
AU - Yukai Song
PY - 2026
DA - 2026/10/03
PB - arXiv
DO - 10.48550/arxiv.2610.04194
UR - https://arxiv.org/abs/2610.04194
AB - We study the largest size C(n) of a subset of the n× n integer grid containing no isosceles triple, including equally spaced collinear triples. We prove C(n)=Ω(n√(loglog n/log n)) by applying the sparse hypergraph coloring theorem of Cooper and Mubayi. Elementary geometry and primitive-direction counts give maximum degree O(n^2log 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 √(loglog 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≤ n≤12; 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.
ER -