🔢 mathematics

Automated conjecturing with \emph{TxGraffiti}

This paper presents the design, core principles, and data-driven methodology of \emph{TxGraffiti}, a computer program that automates the generation of mathematical conjectures—particularly in graph theory—while highlighting its contributions to the literature and introducing a new interactive web interface.

Original authors: Randy Davila

Published 2026-05-12

📖 4 min read🧠 Deep dive

CC0 1.0

Original authors: Randy Davila

Original paper dedicated to the public domain under CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a massive, digital library filled with thousands of different types of puzzles (in this case, mathematical shapes called "graphs"). For every puzzle in the library, mathematicians have already calculated a long list of stats: how many pieces it has, how many connections it makes, and whether it has certain shapes inside it.

TxGraffiti is a smart computer program that acts like a super-organized detective in this library. Its job isn't to solve the puzzles for you, but to look at the stats and guess the rules that govern them.

Here is how it works, broken down into simple steps:

1. The "Snapshot" Library

Instead of the computer trying to calculate stats on the fly (which would be slow), the researchers first take a "snapshot" of the library. They create a giant spreadsheet where every row is a puzzle and every column is a stat. This spreadsheet is the "evidence base." The computer doesn't guess randomly; it only looks at the facts already written in this spreadsheet.

2. The "Guessing Game" (Fitting the Line)

The computer picks one stat it wants to predict (let's call it the "Target," like the number of independent pieces in a puzzle). It then looks at other stats (the "Predictors") to see if they can help guess the Target.

Imagine you are trying to guess how tall a person is (Target) based on their shoe size (Predictor). The computer draws a straight line on a graph that sits just above all the people in the spreadsheet. It tries to make this line as close to the people as possible without ever going below them.

If the line touches a person, that person is a "perfect example" of the rule.
The computer does this mathematically for every possible combination of stats to find the tightest, most accurate "ceiling" (upper bound) or "floor" (lower bound).

3. The "Wall of Fame" Filter (The Dalmatian Heuristic)

The computer generates thousands of these "lines" (rules). Most of them are boring or useless. For example, it might find a rule that is true but so loose it doesn't tell you anything new.

To fix this, TxGraffiti uses a filter called the Dalmatian Heuristic. Think of it like a curator for a museum:

The computer looks at a new rule.
It asks: "Does this rule explain a puzzle that no other rule has explained yet?"
If the answer is yes, the rule gets added to the "Wall of Fame."
If the answer is no (because another rule already covers that puzzle perfectly), the new rule is thrown out as redundant.

This ensures the final list is short, sharp, and contains only the most interesting discoveries.

4. From Guess to Proof

The output of TxGraffiti is a list of conjectures. In math, a conjecture is a "smart guess" that looks true based on the evidence but hasn't been proven yet.

The Workflow: A human mathematician looks at the computer's guess. They check if it makes sense. They try to prove it using logic.
The Success: The paper lists several real-world examples where TxGraffiti made a guess, and human mathematicians later proved it to be a Theorem (a proven fact).
- Example 1: The computer guessed that in certain regular shapes, the number of independent pieces is never larger than the number of matching pairs. Humans proved this is true.
- Example 2: It guessed a relationship between "zero forcing" (a specific way of coloring shapes) and "claw-free" shapes. Humans proved this too.

Why This Matters

Before systems like this, mathematicians had to stare at data for years to find patterns. TxGraffiti automates the "pattern spotting" part. It doesn't replace the human mathematician; instead, it acts like a high-powered telescope, scanning the data to point the human in the direction of the most promising new laws of the universe.

In short: TxGraffiti is a tool that takes a spreadsheet of math facts, draws the best possible lines through them, filters out the boring ones, and hands the remaining "smart guesses" to humans to turn into proven laws.

Technical Summary of "Automated Conjecturing with TxGraffiti"

Problem Statement
The paper addresses the challenge of automated conjecturing: the generation of mathematically useful, non-redundant, and interpretable inequalities among numerical invariants of mathematical objects (specifically graphs). While automated theorem proving is a mature field, automated conjecture generation has historically struggled with the "too-many-statements" problem, where systematic enumeration produces vast numbers of database-true but trivial or redundant statements. The goal is to filter these statements to identify those that offer genuine new information (informativeness) and are suitable for human scrutiny and proof.

Methodology
The paper introduces TxGraffiti (Texas Graffiti), a heuristic- and optimization-based system that operates on a finite, versioned snapshot table of mathematical objects. Unlike its predecessors (Graffiti and Graffiti.pc), which compute invariants dynamically during the search, TxGraffiti treats the evidence base as a static artifact.

The conjecturing pipeline consists of the following stages:

Data Curation (Snapshot Table):
- A table is constructed where rows represent objects (graphs) and columns represent precomputed numerical invariants (e.g., independence number $\alpha$ , matching number $\mu$ ) and Boolean predicates (e.g., "is connected," "is regular").
- The curation strategy prioritizes coverage over randomness, specifically including extremal constructions, equality witnesses (sharp cases), and counterexamples to ensure the table is diagnostically rich.
Candidate Generation via Optimization:
- For a chosen target invariant $\alpha$ and a Boolean predicate $P$ (hypothesis), the system searches for affine bounds of the form $\alpha \le mx + b$ or $\alpha \ge mx + b$ , where $x$ is a predictor invariant.
- Instead of enumerating complex expression trees, TxGraffiti fixes a simple parametric hypothesis class (univariate affine bounds) and fits coefficients by solving Linear Programs (LPs).
- Upper Bound LP: Minimizes total slack $\sum (mx_i + b - \alpha_i)$ subject to $\alpha_i \le mx_i + b$ for all rows satisfying $P$ .
- Lower Bound LP: Maximizes total slack (or minimizes negative slack) subject to $\alpha_i \ge mx_i + b$ .
- The system also supports multivariate bounds and nonlinear relationships by expanding the schema with derived columns (e.g., $n-\mu$ , $\Delta^2$ ), though the default web interface prioritizes single-predictor models for interpretability.
Filtering (Static-Dalmatian Heuristic):
- To manage redundancy, TxGraffiti employs a static-Dalmatian heuristic.
- Touch Number: Defined as the count of objects in the snapshot where the inequality holds with equality (sharp instances).
- Selection Logic: Candidates are sorted by touch number. A candidate is accepted as a "representative" if it touches at least one object not yet covered by the sharp sets of previously accepted representatives. If a candidate's sharp set is identical to an accepted representative's, it is retained as an "alias" (a different syntactic form of the same equality locus). Candidates that add no new sharp instances are discarded.

Key Contributions

System Architecture: TxGraffiti is presented as a modular system available as an interactive web application and an open-source Python package (txgraffiti). It decouples invariant computation from conjecture generation, allowing for rapid iteration on fixed datasets.
Optimization-Based Fitting: The paper shifts the paradigm from grammar-based enumeration (generating formulas and testing them) to optimization-based fitting (solving LPs to find the tightest bounds for specific predictors). This ensures that generated candidates are "table-true" by construction and optimized for tightness.
Static-Dalmatian Filtering: The adaptation of the Dalmatian heuristic to a fixed snapshot allows for a single-pass, deterministic filtering process that prioritizes bounds with high "touch" (many sharp witnesses) while eliminating redundancy.
Interpretability: By restricting the hypothesis class to simple affine templates and rationalizing coefficients, the system produces conjectures that are concise and human-readable.

Results
The paper demonstrates the system's efficacy through several examples:

Workflow Illustration: Using the total domination number $\gamma_t$ , the system generated a bound $\gamma_t(G) \ge \frac{2}{3}R(G)$ for graphs with $\Delta(G) \le 3$ . This was quickly generalized to a theorem involving $\Delta(G)$ and proved using standard estimates.
Stimulated Publications: The paper catalogs several graph-theoretic results that originated as TxGraffiti conjectures and were subsequently proved:
- Independence vs. Matching: The conjecture that $\alpha(G) \le \mu(G)$ for $r$ -regular graphs was proved in [51].
- Zero Forcing Bounds: Several inequalities relating zero forcing numbers ( $Z, Z_t, Z_+$ ) to domination and independence parameters were conjectured and proved, including $Z(G) \le \beta(G)$ for claw-free graphs and bounds for cubic graphs.
- Open Problems: The system identified the conjecture $Z(G) \le \alpha(G) + 1$ for connected graphs with $\Delta \le 3$ , which remains a central open problem, though partial results exist.

Significance and Claims
The paper positions TxGraffiti not as a tool for discovering deep theorems autonomously, but as a structured evidence generator that facilitates human mathematical inquiry.

Empirical Validity: The system produces "table-true" statements, meaning they hold for all instances in the curated snapshot. The authors explicitly reserve the term "theorem" for statements established by formal proof, distinguishing the system's output as conjectures.
Philosophical Stance: Echoing the empirical perspective of Fajtlowicz (who designed Graffiti), the paper argues that the ability of machines to produce plausible, deep conjectures is an empirical fact that supports the view of machines as meaningful participants in open-ended mathematical discovery.
Scalability and Reproducibility: By treating the snapshot table as a versioned, auditable artifact, TxGraffiti addresses the robustness issues of data corruption and ensures that conjectures can be reproduced and refined as the evidence base grows.

The authors conclude that while the current implementation focuses on graph invariants, the "snapshot-table paradigm" and the optimization-and-filtering pipeline are broadly applicable to any domain where objects admit computable features and predicates.