Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design
Hai Xia, Carla P. Gomes, Bart Selman, Stefan Szeider
cs.AI
Mar 9, 2026 · v2
cs.HC math.CO
TL;DR
The tight lower bound 4n(n-1)/9 on Latin square imbalance for n ≡ 1 (mod 3) was formally verified in Lean 4.
Abstract
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.
Problem
The minimum achievable imbalance of n×n Latin squares for n ≡ 1 (mod 3), where perfect spatial balance is impossible, had remained open. The paper also asks how human-AI discoveries unfold at the process level, a question that existing accounts of AI-assisted mathematics leave largely unexamined.
Approach
An LLM agent (Claude Opus 4.5) with terminal access worked alongside symbolic tools and human steering. The tools were SageMath, a custom Rust enumeration solver and simulated annealing. Interaction logs from about fifteen sessions over five days were reconstructed into five phases, and each phase's cognitive contribution was attributed to the agent, the symbolic tools or the human. The bound itself was proved from a fixed-sum lemma and a parity lemma on row-pair distances, then formally verified in Lean 4.
Results
Every n×n Latin square with n ≡ 1 (mod 3) has imbalance at least 4n(n-1)/9. The bound is tight, achieved via a new class of near-perfect permutations found for n up to 52. Multi-model LLM deliberation was reliable for error detection but unreliable for constructive claims, and the key research pivot came from the human.
