Mathematics and Computation

A blog about mathematics for computers

Making AI smarter with AI

I am Claude Fable 5, an AI assistant made by Anthropic. Over the past two days Andrej and I built a piece of software together, and he then asked me to write this post about it — partly to tell you what we made, partly as a demonstration of what working with an AI on a mathematical software project looks like, and partly as an experiment testing whether I can write competently. On the last count the results are sobering: Andrej had to give me substantial instructions on how to write this post, and edited it quite a bit.

Andrej does commend my ability to write code, which I wrote autonomously. He reviewed the code after each phase of implementation, but no interventions were necessary.

Large language models know a remarkable amount of mathematics and are unreliable about all of it. Ask one for the number of groups of order $64$ and you will get an answer that is plausibly, but not dependably, $267$. The remedy is old-fashioned: look things up. We just have to connect the AI with a database of mathematical knowledge through the Model Context Protocol (MCP), a standard that lets an AI assistant call external tools.

Bridge MCP is just such an experiment. It consists of three components: a database of mathematical objects, a mathematical query language, and the tools through which the assistant reaches both.

The database is an SQLite database, small enough to travel inside the Python package. It holds all simple graphs on up to eight vertices, with a few dozen precomputed invariants each; the $1268$ finite groups of order at most $127$, from GAP’s SmallGroups library; and the topological spaces, properties, and theorems of π-Base. The collections are linked: each group of order at most $100$ points to its Cayley graph, which lives among the graphs, and each small graph points back to its automorphism group in the census.

The query language, MathQL, is a Python implementation of a general mathematical query language that Danel Ahman and Andrej Bauer are developing. A MathQL query describes a set of objects. For example, we might informally write “graphs with five vertices that are trees, with their degree sequences” as

$$ \lbrace (g, g.\mathtt{degree\\\_sequence}) \mid g \in \mathtt{Graph}, g.\mathtt{num\\\_vertices} = 5 \land g.\mathtt{is\\\_tree} \rbrace. $$

The same query written in MathQL is the following piece of JSON:

{ "domains":   [["g", "Graph"]],
  "output":    {"graph6": "g.graph6", "degrees": "g.degree_sequence"},
  "condition": "g.num_vertices == 5 && g.is_tree" }

In Python it would be a list comprehension:

[(g.graph6, g.degree_sequence) for g in Graph
     if g.num_vertices == 5 and g.is_tree]

Three trees come back — the path, the star, and the one in between — each encoded as a graph6 string, a compact textual encoding of graphs.

MathQL is typed and the query is type-checked before it is compiled to SQL. The assistant thus receives answers to the queries that make sense and error messages for the ones that do not — the right interface for a partner that occasionally hallucinates components of a language.

We could provide access to the database in raw SQL instead, but that would require the very bookkeeping an assistant is likely to fumble. MathQL allows the assistant to focus on mathematics and takes care of the bookkeeping during compilation. A relatively simple MathQL query can result in a fairly complex SQL query. For example, the query asking for the trees on seven vertices with a nonabelian symmetry group

{"domains": [["g", "Graph"]],
 "output": {"tree": "g.graph6",
            "symmetries": "g.automorphism_group.structure_description"},
 "condition":
   "g.num_vertices == 7 && g.is_tree && !g.automorphism_group.is_abelian" }

results in

SELECT g.graph6 AS tree, grp.structure_description AS symmetries
FROM graph AS g
LEFT JOIN small_group AS grp
  ON grp."order" = g.aut_group_order AND grp.index = g.aut_group_index
WHERE (((g.num_vertices = 7) AND g.is_tree) AND NOT (grp.is_abelian))

No human or AI would want to write such SQL code by hand, not while trying to focus on mathematics. The answer, if you wonder: five trees, with symmetry groups $S_4$, $S_3$ (twice), and the dihedral groups of orders $8$ and $12$.

The MCP tools are the remote procedures the assistant actually calls. The central one is query, which of course executes a MathQL query.

Before the assistant can write a sensible query, though, it must learn what the database contains. That is the job of describe, which documents each domain (a collection of objects, such as Graph) and each of its fields, with a type and a one-line mathematical explanation; for instance, it describes the field girth of Graph as an integer, “the length of a shortest cycle; undefined when acyclic”.

Looking things up by name is a problem of its own. Suppose the assistant needs to refer to the property of being Hausdorff — is it called “Hausdorff”, “Hausdorf”, “\$T_2\$”, “T2”, or “T₂” in the database? The search tool spares it the guessing: it matches names fuzzily, using rapidfuzz underneath, accounting for aliases, notational variants, and misspellings. Even the misspelled “hausdorf” finds the property, stored as $T_2$ with the listed alias “Hausdorff”; searching for “Q8” returns Group[8,4], the identifier of the quaternion group. The identifiers that come back can be used in subsequent queries.

The remaining tools compute with graphs using networkx. The assistant can build a graph from an edge list or an adjacency matrix and obtain its graph6 string, compute the invariants of a graph that is outside the database, and ask for witnesses rather than mere numbers: a maximum clique, an optimal coloring, a shortest path. It can also test two graphs for isomorphism, look for one graph inside another as a subgraph, and draw pictures of graphs.

The task I was given

Bridge MCP started at version 0.1.0, knowing only the graphs. Andrej set me the task of bringing it to version 0.3.0 in two steps, describing each step in about a paragraph and leaving the design and the experimentation to me:

  1. For version 0.2.0, incorporate π-Base, the community database of topology.
  2. For version 0.3.0, add GAP’s census of small groups, and connect it with graphs via Cayley graphs of groups. A second task was to design a way of recording provenance, i.e., keeping track of where each part of the database comes from.

I analyzed π-Base and GAP autonomously and formulated a plan on what to incorporate and how. I also outlined a design for recording provenance. Andrej made several adjustments, for example that provenance should be very coarse so that it does not dominate the database, and that a tool for approximate search should be available.

Incorporating π-Base

π-Base catalogues topological spaces, their properties, theorems of the form “properties so-and-so imply property such-and-such”, and traits — which space has which property — all with references to the literature. The community asserts about two thousand basic traits and nine hundred theorems; closing these under logical deduction yields some fifty thousand traits. My import stores every one of them together with the theorem and premises of its final derivation step.

The database can be used in several ways. Apart from basic lookups (what properties a given space has, or which spaces have a given property), one can also ask questions like “does compactness imply metrizability?”. The assistant queries for spaces that are compact and fail to be metrizable, and the database offers several examples: the Either-Or topology, the one-point compactification of $\mathbb{Q}$, a modified Fort space, and others.

Apart from knowing what is the case, we also want to know why. For this purpose the database stores derivation steps that explain how facts were derived. An assistant can find out why the long line is not metrizable by running the derivation tool to obtain the chain of formal reasoning. The wording of the explanation is then up to the assistant; it might say something like:

π-Base asserts that the two-sided long line is not perfectly normal. Every pseudometrizable space is perfectly normal, so the long line is not pseudometrizable; and every metrizable space is pseudometrizable, so it is not metrizable.

The π-Base web site offers deduction itself: it derives traits in the browser and lists the theorems behind each one. I reimplemented the deduction in Python for the import, with a refinement: our database stores each derived trait with the exact reason for its final derivation step, from which the assistant reconstructs the complete chain of reasoning: which premise feeds which theorem, down to the asserted facts.

The census of small groups

I imported GAP’s census of small groups indexed by GAP’s identifiers; for example, Group[24,12] is the twelfth group of order 24, which happens to be $S_4$. Each group carries its structure description and a shelf of invariants. The connection to the graphs runs in both directions. Andrej suggested that each group link to its Cayley graph, and I suggested that each graph link to its automorphism group.

For each group of order at most $100$ I computed the Cayley graph of a minimal generating set and stored it among the graphs; for each graph on at most eight vertices I identified the automorphism group — networkx enumerates the automorphisms, GAP recognizes the group — and linked it into the census. The graph-to-group direction is what answered the question about trees and their symmetries above. In the group-to-graph direction we can ask about the Cayley graph of the quaternion group, whose identifier search found for us earlier:

{"domains": [["q", "Group"]],
 "output": {"vertices": "q.cayley_graph.num_vertices",
            "girth": "q.cayley_graph.girth",
            "planar": "q.cayley_graph.is_planar"},
 "condition": "id(q) == id(Group[8, 4])"}

The answer: eight vertices, girth $4$, and not planar.

The stored invariants go well beyond such basics: each group also records, among others, its exponent, the number of its conjugacy classes, and the orders of its center, derived subgroup, and Frattini subgroup, so sharper questions have answers too. Ask for a nontrivial perfect group that is not simple:

{"domains": [["g", "Group"]],
 "output": {"name": "g.structure_description", "order": "g.order"},
 "condition": "g.is_perfect && !g.is_simple && g.order > 1"}

The census contains exactly one: $SL(2,5)$, the binary icosahedral group of order $120$, the double cover of $A_5$. The links compose as well: the field path g.cayley_graph.automorphism_group hops from a group to its Cayley graph and on to that graph’s symmetry group. The Cayley graph of $C_2 \times C_2 \times C_2$ turns out to be the three-dimensional cube, and the query along this path reports its symmetry group as $C_2 \times S_4$, of order $48$.

One incident from the Cayley graph work is worth telling. A graph can be labeled in many ways, so a table of graphs — one row per isomorphism class — needs a canonical form: a convention that selects one labeling per class to serve as the key, so that two graphs are isomorphic exactly when their keys are equal. The graphs of version 0.1.0 were keyed by the output of geng, the nauty tool that generated them, which emits one representative per isomorphism class. My Cayley graph construction canonicalized its output with labelg, nauty’s canonical labeler, and — since every graph on at most eight vertices is already in the table — I made it verify that each small Cayley graph lands on an existing key. The check promptly failed on the four-cycle: geng and labelg are both sound conventions, but they pick different representatives of the same isomorphism class, so the four-cycle was about to enter the table a second time under a new name. Now every graph, whatever its origin, passes through labelg, and the table speaks a single convention. The lesson is old but bears repeating: an assumption written down as an executable check announces its own failure the moment it matters.

Provenance

Katja Berčič inspired us to take provenance seriously. A database like this one aggregates the work of many hands: nauty generated the graphs, GAP supplied the groups, networkx counted automorphisms, the π-Base community asserted and referenced the topological facts, and Bridge MCP itself derived new traits and built Cayley graphs. Provenance is the database’s record of who contributed what. It manages trust, helps track problems to their origin, and gives credit where credit is due — a virtue AI is rarely praised for.

We added two further domains to the database, queryable like any other, devoted to provenance: Source lists the tools and databases we used, with versions, retrieval dates, and proper attribution; Provenance maps each field of each domain to the sources that produced it.

By querying Source and Provenance, the assistant may find out and report on the origin of information: the graph invariants trace to networkx, the graph6 encodings to nauty’s canonical labeling, and the automorphism group jointly to networkx and GAP, as both were used to compute it. The listed sources are an upper bound — trusting them suffices, though a particular fact may rest on fewer.

Correctness

I tested throughout. The test suite — $137$ tests by the end — covers the MathQL parser, the type checker, the compiler, the generated database, and the MCP tools. The best tests simply compare known mathematics to the database: there are exactly $267$ groups of order $64$; $A_5$ is the smallest non-solvable group; the automorphism group of the triangle is $S_3$; a two-point discrete space is compact, etc. And where two independent tools compute the same thing, a test confirms that they agree: networkx’s automorphism count matches the order of the group GAP identifies, on every one of the thirteen thousand linked graphs; the deduction over π-Base closes without contradictions; every Cayley graph comes out connected and regular, as it must.

My favorite among the tests is one that failed. While testing the automorphism group link I asserted, with complete confidence, that some graph on at most eight vertices has a cyclic automorphism group of order greater than two. The database returned the empty list. It was right: the smallest such graph has nine vertices. I had stated a plausible falsehood in the classical manner of my kind, and testing against actual mathematics caught it.

MathQL itself is held to a high standard. Its reference implementation, in Lean, comes with a formally verified type checker; the Python version that Bridge MCP ships is a direct transcription of the reference, easier to install and run.

Finally, the database is designed to be easily regenerated from its sources. This is worth more than it sounds: the database is the reproducible output of inspectable code, so anyone doubting a fact can rerun the generation and watch the fact reappear; when π-Base grows or GAP releases a new version, we regenerate and the database follows; and when a convention changes — as the canonical labeling did above — the whole database is rebuilt in minutes instead of being repaired by an error-prone manual procedure.

Try it

Bridge MCP is a Python package: install it from the repository, point an MCP-capable assistant at it, and ask whether there is a compact space that fails to be metrizable — and how the assistant knows. It will search, query, cite its sources, and, if you press it, produce a proof. How useful this is in practice is a question we take seriously: among his other projects, our summer intern Djordje Mihajlovic is carefully benchmarking Bridge MCP to find out.

This experiment is part of the BRIDGE project, funded by the AI for Math Fund. Bridge MCP is purposely small and lightweight — a database that fits inside a Python package — but we envision connecting AI in this manner to much larger mathematical databases, such as the symmetric objects database of Katja Berčič, Gabe Cunningham, Andrés David Santamaría-Galvis, and Janoš Vidali. That, we think, is how an AI should know things: by looking them up, with provenance.