Andrew Curtis Conjecture.

A Neuro-Symbolic Approach

This section introduces the core mathematical puzzle at the heart of our research. Here you will learn what the Andrews-Curtis conjecture is, the components that define it, and how the rules it uses fit within a broader hierarchy of mathematical transformations. Understanding these fundamentals is key to appreciating the complexity of the problem and the novelty of AI-driven approaches.

The Andrews-Curtis Conjecture

At its core, the conjecture proposes that any **balanced presentation** of the **trivial group** can be simplified to a basic form using a very restricted set of moves.

Balanced Presentation: When the number of generators (symbols) equals the number of relators (rules).

Example: <x, y | xyx=yxy, x³=y²> has 2 generators (x, y) and 2 relators, so it's balanced.

Trivial Group: A group where the relators are so powerful they force every element to be the identity (like '1' in multiplication).

Example: <x | x³=1, x⁵=1>. The only integer solution is x=1, so the group is trivial.

The AC conjecture asks: Can we always prove a group is trivial using only a few simple relator manipulations, or are there 'impostor' presentations that look complicated but are secretly trivial, yet can't be simplified with these limited tools?

Hierarchy of Transformations

The difficulty of the AC conjecture comes from its restrictive rules. Click the buttons below to see the formal definitions of each toolkit for manipulating a set of relators {r₁, r₂, ...}.

Standard AC Moves

A highly restricted set of three moves operating on the list of relators:

  1. Inversion: Replace any rᵢ with its inverse rᵢ⁻¹.
  2. Multiplication: Replace any rᵢ with rᵢrⱼ (for i ≠ j).
  3. Conjugation: Replace any rᵢ with g⁻¹rᵢg (for any generator g).

Connection to Geometry: Each presentation can be viewed as a recipe for constructing a 2D topological space (a 2-complex). This turns an abstract algebra problem into a geometric one: can these spaces always be collapsed to a point using a very restricted set of moves?

An Example in Transformations

Let's see how different toolkits handle the trivial presentation <x, y | x, xy>. Our goal is to reach the simplest form: <x, y | x, y>.

Result: No Progress

This is a crucial point. Even though we know x is a relator (so x=1), the standard AC moves do not allow us to *substitute* that information into other relators. AC moves manipulate the relators themselves (e.g., replacing r₂ with r₂r₁), not parts of them. Substituting x with 1 inside xy is a Tietze move, not an AC move. We are stuck.

Result: Solved

The Stable AC conjecture allows adding a new generator and relator (e.g., z and z). This extra 'workspace' unlocks the solution:

  1. Start: {x, xy}
  2. Add z: {x, xy, z} (Now using 3 relators for 3 generators)
  3. Multiply z by x: {x, xy, zx}
  4. Multiply (xy)⁻¹ by zx: {x, xy, y⁻¹x⁻¹zx}
  5. ... (further steps) ... can eventually isolate y.

Connection to Topology: This "stabilization" move is deeply connected to 4-manifold topology. It's the algebraic equivalent of allowing higher-dimensional geometric moves to untangle knots, linking this conjecture to the fundamental structure of 4D spaces.

Result: Solved Trivially

Tietze transformations are the most powerful. They allow us to define new relators from existing ones. The solution is direct:

  1. Start: {x, xy}
  2. Since x=1 (from the first relator), we can substitute it into the second relator: (1)y = y.
  3. Add this new consequence as a relator: {x, xy, y}.
  4. Now remove the redundant relator xy.
  5. Finish: {x, y}.

The Andrews-Curtis conjecture is not an isolated curiosity. It sits at a crossroads of algebra and geometry, deeply connected to some of the most famous unsolved problems in low-dimensional topology. A solution, or even a counterexample, would have significant repercussions in these related fields.

Smooth 4D Poincaré Conjecture

This famous conjecture states that any 4-dimensional manifold that "looks like" a sphere (a homotopy 4-sphere) can be smoothly deformed into one. A balanced presentation of the trivial group is a recipe for building exactly such a manifold.

The Connection:

If a presentation is AC-trivial, the resulting manifold is the standard 4-sphere. A counterexample to the AC conjecture could potentially be used to construct an "exotic" 4-sphere—a manifold that looks like a sphere but isn't—which would disprove the Poincaré conjecture.

Knot Theory & Slice-Ribbon

Knot theory studies the mathematical properties of knots in 3D space. A key question is which knots can be the boundary of a smooth disk in 4D space (a "slice" knot). The Slice-Ribbon conjecture asks if every slice knot is a simpler type of knot called a ribbon knot.

The Connection:

Many potential AC counterexamples are generated through complex topological procedures on knots and links (like Dehn surgery). Proving a presentation is trivial often involves showing an associated link is "slice," tying the algebraic problem of AC moves directly to the geometric problem of untangling knots in four dimensions.

The Whitehead Conjecture

This is a purely topological conjecture about the structure of 2-complexes (the geometric objects built from presentations). It asks whether any sub-complex of an "aspherical" 2-complex is also aspherical. Aspherical means the space is connected but has no "holes" in higher dimensions.

The Connection:

While distinct from the AC conjecture, it lives in the same intellectual space. Both conjectures are fundamentally about whether the simple algebraic data of a presentation forces a complex geometric structure to be simple in some way (AC: contractible to a point; Whitehead: having no higher-dimensional holes).

The search space for solving the AC conjecture is astronomically large, making brute-force methods impossible. This section explores how two complementary AI systems tackle this "needle-in-a-haystack" problem. One acts as a powerful "Pathfinder" to discover solutions, while the other serves as a rigorous "Verifier" to mathematically guarantee their correctness.

The Computational Challenge

The shortest path to simplify a presentation can be a superexponential function of its length.

The "Pathfinder" Agent

Sergei Gukov and team developed a Reinforcement Learning agent to take a known trivial presentation and discover the explicit sequence of AC moves that simplifies it. It learns a policy for selecting moves to reach the goal state.

Key Reported Results:

  • Solved families of potential counterexamples that had been open for over 25 years.
  • Proved that the famous Akbulut-Kirby `AK(3)` presentation is stably AC-trivial, resolving a major open case.
  • Discovered solution paths with over 8,000 steps, far beyond what brute-force search could ever find.

The "Verifier" Auto-formalizer

Our work provides the crucial final step: rigorous verification. We developed a tool that takes a path found by an agent and automatically generates a formal, machine-checkable proof in the Lean proof assistant.

Role: Path-Checker

Method: Auto-formalization to Lean

Success: Successfully formalized the conjecture and verified large datasets of solved presentations.

Limitation: Can only certify concrete, finite paths, not prove general theorems about infinite families.

AC Agent Path
→
Auto-formalizer
→
Formal Proof

Building on our previous work, the next phase of research focuses on discovery. The goal is to create a robust, neuro-symbolic pipeline capable of generating novel, interesting, and mathematically verifiable candidates for the Andrews-Curtis conjecture. This involves three major steps: generating new problems, discovering general theorems, and expanding the search to new mathematical spaces.

Part 1: Generative Discovery

We will build a system to generate new, likely-trivial presentations that are not in our current dataset. This involves an RL agent exploring a latent space of presentations, guided by a powerful mathematical oracle.

The Feedback Loop:

1. GRPO Agent Proposes Vector
↓
2. Decode to Presentation String
↓
3. GAP Oracle Checks & Rewards ▼
↓
4. Agent Policy is Updated

Part 2: Theorem Discovery

A key challenge with using Large Language Models (LLMs) for mathematical discovery is that they can "hallucinate" or over-generalize, leading to incorrect conjectures. Our next step addresses this directly.

We will implement a more sophisticated, neuro-symbolic approach inspired by recent advances. This system will be designed to not just find patterns, but to ground its discoveries in formal logic, significantly reducing the risk of generating false theorems and ensuring the outputs are more easily verifiable.

Expected Output:

This process aims to generate novel, verifiable conjectures about infinite families of group presentations, moving beyond the verification of single instances towards true mathematical discovery.

Part 3: Expanding the Search Space

Most classical potential counterexamples to the AC conjecture live in F₂, the free group with two generators (e.g., x, y). However, the stable version of the conjecture naturally invites exploration into higher-rank free groups (F₃, F₄, etc.) by allowing the addition of new generators.

This opens a new frontier for AI-driven discovery. An agent is not limited to human intuition and can systematically explore these vastly larger, higher-dimensional search spaces. It's possible that the properties of "hard" presentations change in higher ranks, or that adding and removing generators provides novel pathways for simplification that are not obvious in F₂.

Future Research Questions:

  • Can an RL agent discover new families of trivial presentations that only exist in Fₙ for n > 2?
  • Does the "hardness" of a problem change when embedded in a higher-rank group?
  • Can we train a generative model to produce novel, hard presentations specifically for F₃ and beyond?