用于数学发现的代理神经符号协作：组合设计案例研究

本文通过神经符号推理视角研究数学发现过程，展示了由大语言模型驱动的智能体、符号计算工具与人类战略指导协作，在组合设计理论中取得新成果。主要贡献是针对困难情形$n \≡ 1 \\pmod{3}$的拉丁方不平衡性提出了紧下界。研究重构了跨多天的交互日志，分析了各组件的认知贡献：AI 擅长揭示隐藏结构与生成假设，符号组件提供严谨验证，人类引导关键转折。实验表明神经符号系统能产生真正的纯数学发现，该下界已在 Lean 4 中形式化验证。