Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design

Hai Xia, Carla P. Gomes, Bart Selman, Stefan Szeider

TL;DR

The experiments show that neurosymbolic systems can indeed produce genuine discoveries in pure mathematics, and reveal that multi-model deliberation among frontier LLMs proved reliable for criticism and error detection but unreliable for constructive claims.

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.

Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design

TL;DR

The experiments show that neurosymbolic systems can indeed produce genuine discoveries in pure mathematics, and reveal that multi-model deliberation among frontier LLMs proved reliable for criticism and error detection but unreliable for constructive claims.

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 . 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 , 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.
Paper Structure (25 sections, 5 theorems, 3 equations, 1 figure, 2 tables)

This paper contains 25 sections, 5 theorems, 3 equations, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Problem Setting
  3. The Discovery Process
  4. Dead End: Algebraic Reverse-Engineering
  5. The Research Pivot
  6. Parity from Data Anomaly
  7. Formalization and Multi-Model Review
  8. The circulant trap.
  9. The $\sigma$/$\sigma^{-1}$ mismatch.
  10. Multi-model reliability.
  11. Computational Extension
  12. Persistent Learning Across Sessions
  13. The Mathematical Result
  14. The Lower Bound
  15. The Matching Construction
  16. ...and 10 more sections

Key Result

Lemma 1

For every $n \times n$ Latin square $L$, $\sum_{r_1 < r_2} d(r_1,r_2) = n^2(n^2-1)/6$.

Figures (1)

  • Figure 1: Collaboration architecture and data flow. Rounded boxes represent actors (human, agent, symbolic tools); italic labels on arrows show the data exchanged. Solid arrows indicate instructions or code sent; dashed arrows indicate results returned. The AI agent orchestrates all interaction: it dispatches proof drafts to parallel frontier LLMs for critical review (left) and maintains a three-component persistent memory (right) comprising a project state file, a searchable knowledge base of topic files, and a session handover protocol.

Theorems & Definitions (10)

  • Lemma 1: Fixed sum
  • proof
  • Lemma 2: Parity
  • proof
  • Theorem 3
  • proof
  • Definition 4
  • Proposition 5
  • proof
  • Theorem 6