发表机构
University of Pittsburgh（匹兹堡大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究通过稀疏超图染色定理证明无等腰三元组的网格子集大小下界，改进PatternBoost的保证，并分析AI辅助证明过程中的检查实践。
AI 中文摘要
我们研究$n\times n$整数网格中不含等腰三元组（包括等距共线三元组）的子集的最大大小$C(n)$。通过应用Cooper和Mubayi的稀疏超图染色定理，我们证明$C(n)=\Omega\left(n\sqrt{\log\log n/\log n}\right)$。初等几何和原始方向计数给出禁止三元组超图的最大度为$O(n^2\log n)$，配对余度至多$5n$。所得界将PatternBoost中的显式保证改进了一个$\sqrt{\log\log n}$量级的因子。恢复的交互记录记录了Codex文献提议、人工路线选择、有限验证和作者转达的评审如何为证明综合与修复提供信息。我们将这些行动与连续的证明产物联系起来，并提取两种从案例中得出的检查实践：在定理应用中跟踪对象、参数和结论，以及播种一个定义遗漏来测试有限验证器。分别实现的枚举器对每个$2\le n\le12$的完整边集达成一致；抑制退化情况分支恰好丢失等距共线三元组。这些记录记录了在人工指导下的辅助，有限检查支持实现一致性而非渐近定理本身。
英文摘要
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)=Ω\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.
Comments8 pages, 2 tables. Accepted for poster presentation at the NeurIPS 2026 MATH-AI Workshop. Verification code and results are included as ancillary files
