We study mathematical discovery through the lens of neurosymbolic reasoning, where an AI agent powered by a large language model (LLM), coupled with symbolic computation tools, and human strategic direction, jointly produced a new result in combinatorial design theory. The main result of this human-AI collaboration is a tight lower bound on the imbalance of Latin squares for the notoriously difficult case $n \equiv 1 \pmod{3}$. We reconstruct the discovery process from detailed interaction logs spanning multiple sessions over several days and identify the distinct cognitive contributions of each component. The AI agent proved effective at uncovering hidden structure and generating hypotheses. The symbolic component consists of computer algebra, constraint solvers, and simulated annealing, which provides rigorous verification and exhaustive enumeration. Human steering supplied the critical research pivot that transformed a dead end into a productive inquiry. Our analysis reveals that multi-model deliberation among frontier LLMs proved reliable for criticism and error detection but unreliable for constructive claims. The resulting human-AI mathematical contribution, a tight lower bound of $4n(n{-}1)/9$, is achieved via a novel class of near-perfect permutations. The bound was formally verified in Lean 4. Our experiments show that neurosymbolic systems can indeed produce genuine discoveries in pure mathematics.

翻译：本研究从神经符号推理的视角探讨数学发现过程，其中由大型语言模型（LLM）驱动的智能体、符号计算工具与人类战略指导协同合作，在组合设计理论中取得了新成果。此次人机协作的核心成果是针对长期悬而未决的$n \equiv 1 \pmod{3}$情形，给出了拉丁方不平衡度的紧致下界。我们通过分析历时数日、跨越多个会话的详细交互日志，重构了发现过程并识别了各组成部分的认知贡献。智能体在揭示隐藏结构和生成假设方面表现出色；符号计算组件（包括计算机代数系统、约束求解器和模拟退火算法）提供了严格验证与穷举枚举；人类引导则通过关键的研究转向将死胡同转化为有效探索。分析表明，前沿LLM间的多模型审议机制在批判与错误检测方面可靠，但在建设性主张方面存在局限。最终通过构建新型近似完美置换类，获得了紧致下界$4n(n{-}1)/9$，该结果已在Lean 4中完成形式化验证。实验证明神经符号系统确实能够在纯数学领域实现实质性发现。