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

This paper presents a neurosymbolic collaboration between an LLM-powered agent, symbolic computation tools, and human researchers that successfully discovered and formally verified a new tight lower bound on the imbalance of Latin squares for the case $n \equiv 1 \pmod{3}$, demonstrating the potential of AI-human partnerships in pure mathematical discovery.

The Gist

Imagine a team of three explorers trying to solve a massive, locked treasure chest in a dense jungle. The chest is a famous unsolved math problem about Latin Squares (think of them as giant, perfect Sudoku puzzles where every number appears exactly once in every row and column).

The team consists of:

1. The Human Captain: A seasoned researcher with a map and a compass.
2. The AI Scout: A super-fast, pattern-spotting drone powered by a Large Language Model (LLM).
3. The Symbolic Engine: A heavy-duty, unyielding robot that does exact calculations and checks every single possibility.

Here is the story of how they worked together to find the treasure, told in simple terms.

The Problem: The "Perfect" Puzzle That Doesn't Exist

The explorers were looking for a specific type of Latin Square that was perfectly balanced. For most sizes, this is possible. But for squares where the size ($n$) leaves a remainder of 1 when divided by 3 (like 4, 7, 10, 13...), math says a "perfectly balanced" square is impossible.

The question was: "If we can't make it perfect, what is the closest we can get?"

Phase 1: The Wrong Turn (The Dead End)

At first, the AI Scout tried to use old-school algebra to build these perfect squares from scratch. It ran thousands of simulations, looking for a secret formula.

• The Result: Nothing. The AI found that for larger numbers, the patterns looked like "white noise" or static on a TV screen. There was no hidden algebraic structure to find.
• The Lesson: The AI was good at checking, but it was stuck trying to solve a problem that might not have a "perfect" solution.

Phase 2: The Human Pivot (The "Aha!" Moment)

This is where the Human Captain stepped in. While the AI was busy trying to build a perfect square, the Captain realized they were asking the wrong question.

• The Shift: Instead of asking, "How do we make a perfect square?" the Captain asked, "What is the minimum amount of imperfection we can tolerate?"
• The Metaphor: Imagine you are trying to build a tower of blocks that is perfectly straight. You realize it's impossible. Instead of giving up, you ask, "What is the smallest wobble I can accept?" This changed the mission from "Find the impossible" to "Find the best possible."

Phase 3: The AI's Superpower (Spotting the Hidden Clue)

With the new goal, the AI Scout went back to the data. It looked at thousands of "imperfect" squares generated by the Symbolic Engine.

• The Discovery: The AI noticed something weird that a human would likely miss without a computer: Every single distance between rows was an even number.
• The Analogy: It's like noticing that every time you try to walk across a bridge, you always take an even number of steps, never an odd one. This "parity" rule was the key.
• The Proof: Because the numbers had to be even, the "wobble" (imbalance) couldn't be just a tiny bit off; it had to be twice as big as the AI originally thought. The AI quickly wrote a proof for this new, tighter limit.

Phase 4: The Reality Check (The Critic vs. The Builder)

The team didn't trust the AI's proof immediately. They used a technique called Multi-Model Deliberation.

• The Process: They asked four different AI models to act as "critics" and tear the proof apart.
• The Result: The critics were amazing! They found two subtle mistakes (like confusing the order of operations in a recipe).
• The Twist: When the team asked the AI to predict how well a new method would work, the AI was confidently wrong.
• The Lesson: AI is a great editor (critic) but a risky author (builder). It's excellent at finding errors in others' work but tends to hallucinate when trying to invent new, complex solutions on its own.

Phase 5: The Final Treasure

Using the corrected proof and the Symbolic Engine (which ran a high-speed search called "Simulated Annealing"), the team found a new type of permutation they called "Near-Perfect Permutations."

• They proved mathematically that the minimum "wobble" for these puzzles is exactly $4n(n-1)/9$.
• They verified this up to size 52 using the computer.
• They even wrote the proof in Lean 4, a digital language that forces the computer to check every logical step, ensuring the math is 100% bulletproof.

The Big Takeaway

This paper isn't just about a math puzzle; it's about how humans and AI should work together.

1. The Human provides the strategy. They know when to quit a dead end and change the question. AI is great at following orders, but it doesn't know when to stop and think, "Maybe this path is wrong."
2. The AI provides the pattern recognition. It can scan millions of data points in seconds to find a hidden rule (like the "even number" trick) that a human would take years to spot.
3. The Symbolic Tools provide the truth. They do the heavy lifting and rigorous checking to ensure the AI's wild guesses are actually facts.

In short: The human steered the ship, the AI spotted the hidden island on the radar, and the robot engine navigated the rough waters to get there. Without any one of them, the treasure would have remained lost.

Technical Summary

Here is a detailed technical summary of the paper "Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design."

1. Problem Setting

The paper addresses a fundamental open problem in combinatorial design theory: determining the minimum possible imbalance of Latin squares for the specific case where the order $n \equiv 1 \pmod 3$.

• Latin Squares: An $n \times n$ array filled with $n$ symbols such that each symbol appears exactly once in every row and column.
• Imbalance ($I(L)$): A metric measuring spatial balance, defined as:
  $$I(L) = \frac{1}{3} \sum_{0 \le r_1 < r_2 \le n-1} |3 \cdot d(r_1, r_2) - n(n+1)|$$
  where $d(r_1, r_2)$ is the sum of absolute differences between the positions of symbols in two rows.
• The Challenge:
  • If $n \not\equiv 1 \pmod 3$, perfect balance ($I(L)=0$) is achievable.
  • If $n \equiv 1 \pmod 3$, the ideal distance $n(n+1)/3$ is not an integer, making perfect balance impossible.
  • Prior to this work, the tight lower bound for the minimum positive imbalance in this specific modular case was unknown.

2. Methodology: Agentic Neurosymbolic Collaboration

The authors propose a framework where a Large Language Model (LLM) agent orchestrates a collaboration between symbolic computation tools and human strategic direction.

Architecture

• The Agent: Powered by Claude Opus 4.5, operating in a terminal with access to a file system and external tools.
• Symbolic Tools:
  • SageMath: For computer algebra and exact arithmetic.
  • Rust Solver: A custom high-performance solver for exhaustive enumeration of combinatorial objects.
  • Simulated Annealing (Python): For stochastic optimization to find near-optimal structures.
• Human Role: Provides strategic direction, decides when to pivot research questions, and acts as a quality controller.
• Persistent Memory: A two-tier system (project state file + searchable topic files) allows the agent to maintain context across multiple sessions without updating model weights, enabling "incremental learning."
• Multi-Model Review: Parallel consultation with frontier LLMs to critique proofs and detect errors.

The Discovery Process (5 Phases)

1. Dead End (Algebraic): The agent attempted to find algebraic constructions for "perfect permutations" (yielding zero imbalance). Symbolic analysis revealed these objects lack algebraic structure for $n \ge 6$, leading to a documented dead end.
2. Research Pivot (Human): The human researcher reframed the problem from "finding zero-imbalance objects" to "characterizing the minimum positive imbalance."
3. Pattern Discovery (Agent): The agent analyzed numerical data from simulated annealing runs. It noticed a parity constraint: all shift correlations were even numbers. This led to the hypothesis that the minimum deviation is 2 (not 1), doubling the naive lower bound.
4. Formalization & Review: The agent drafted a proof. Multi-model review caught two critical errors:
   • Overgeneralization: The proof initially relied on circulant structures but claimed generality for all Latin squares.
   • Index Mismatch: A subtle error regarding row distances determined by $\sigma^{-1}$ vs. $\sigma$.
5. Computational Extension: The agent introduced "near-perfect permutations" (where shift correlations are $a$ or $a+2$) and used simulated annealing to verify their existence up to $n=52$, achieving the theoretical bound.

3. Key Contributions

A. Mathematical Discovery

• Tight Lower Bound: Proved that for $n \equiv 1 \pmod 3$, the imbalance satisfies:
  $$I(L) \ge \frac{4n(n-1)}{9}$$
• Near-Perfect Permutations (Near-PP): Introduced a new class of permutations where shift correlations $f_\sigma(\delta) \in \{a, a+2\}$. These structures achieve the lower bound exactly.
• Formal Verification: The main theorem and lemmas were formally verified in Lean 4 using the Mathlib library.

B. Framework Contributions

• Neurosymbolic Workflow: Demonstrated a viable workflow where LLMs handle pattern recognition and hypothesis generation, while symbolic tools handle rigorous verification and exhaustive search.
• Persistent Memory: Showed that a structured, external memory system allows LLM agents to conduct multi-session research effectively without fine-tuning.
• Asymmetry in Deliberation: Identified that multi-model deliberation among frontier LLMs is highly reliable for criticism (error detection) but unreliable for constructive claims (generating new mathematical truths).

4. Key Results

• Theorem: For $n \equiv 1 \pmod 3$, $I(L) \ge 4n(n-1)/9$.
• Existence: Near-perfect permutations exist for all $4 \le n \le 52$(where$n \equiv 1 \pmod 3$), achieving the bound exactly.
• Efficiency: The discovery of the parity constraint and the subsequent proof took less than one hour of agent runtime once the research pivot occurred.
• Comparison: Previous computational work failed to reach the optimum even at $n=10$; the new method reached $n=52$.

5. Significance and Analysis

• Genuine Discovery: This is a rare example of an AI system contributing to a new mathematical result in pure mathematics where the hypothesis was not pre-defined but emerged from the interaction.
• Role Differentiation:
  • Agent: Excelled at uncovering hidden structures (parity) from noisy numerical data and drafting proofs.
  • Symbolic Tools: Provided the "ground truth" via exhaustive search and exact arithmetic, verifying negative results (absence of structure) and positive results.
  • Human: Provided the critical meta-cognitive pivot. The agent continued productively within the wrong frame (searching for zero imbalance) until the human redirected the inquiry.
• Failure Modes:
  • Agents can be confidently wrong (e.g., claiming modular inversion achieves $O(n^{5/2})$ imbalance when it is $\Theta(n^{3.6})$).
  • Symbolic solvers hit combinatorial walls (e.g., $n=18$) due to exponential search space growth.
  • Humans are currently essential for recognizing when a research direction is a dead end.

Conclusion

The paper concludes that neurosymbolic systems can produce genuine mathematical discoveries, but they require a specific division of labor: neural components for intuition and pattern recognition, symbolic components for rigor and verification, and human components for strategic direction and meta-cognitive oversight. The study highlights that while AI is a powerful collaborator, it currently lacks the ability to autonomously recognize when a research path is unproductive.