Can AI write serious mathematics?

A worked example in graph minors and modal logic

A lot of people, often correctly, describe AI-generated math as confident garbage. I agree—if you use AI like autopilot.

This post is about a different workflow: using AI like a very fast, very fallible collaborator, and then applying normal mathematical hygiene—definitions, counterexamples, proofs, and citations—until the result is something you can show to serious mathematicians without cringing.

I’m going to do one complete case study from scratch. This case study was suggested to me as a math problem by Professor Joel David Hamkins. And so, it was not artificially designed for LLMs.

Claim.
Consider the Kripke frame whose worlds are all simple graphs (finite or infinite), and where accessibility is the graph minor relation:

\(G \le H \quad\text{if and only if}\quad G \text{ is a minor of } H.\)

Interpret propositional variables as parameter-free first-order sentences in the pure graph language with a single relation symbol E(x,y) (adjacency), and interpret ◇ and □ using ≤.

Then the exact propositional modal validities of this system are S4.2.

The goal here isn’t just the theorem. It’s to show how AI can help you produce a clean, nontrivial, citation‑backed argument — and also to show where AI will predictably mess up unless you force it to check itself.

---

Prerequisites

Graphs

A simple graph is a set of vertices with an undirected adjacency relation E(x,y), with no loops and no multiple edges.

We’ll only use the fact that graphs can be glued together by disjoint union:

• G ⊔ H means “take both graphs as separate components.”

Graph minors

Intuitively, G is a minor of H if G can be obtained from H by repeatedly:

• deleting vertices,

• deleting edges,

• contracting edges (and then simplifying to stay simple).

For infinite graphs, the clean way to define this is via branch-set models (this is the notion I’ll use):

G ≤ H if there is a map μ: V(G) → 𝒫(V(H)) such that

1. each μ(v) is nonempty and induces a connected subgraph of H,

2. the μ(v) are pairwise disjoint,

3. if vw is an edge of G, then there is an edge of H with one endpoint in μ(v) and one in μ(w).

Think of each vertex of G as a connected “blob” inside H; edges of G are realized by edges between blobs.

Subdivisions

To subdivide an edge uv means: delete the edge uv, add a new vertex w, and add edges uw and wv.

A subdivision of a graph H is any graph obtained by subdividing some edges of H (possibly repeatedly). Equivalently, each edge of H is replaced by a path between the same endpoints, and the internal vertices of these replacement paths are new and internally vertex‑disjoint across different edges (in particular they have degree 2 in the subdivided graph).

Modal logic

A Kripke frame is a set of worlds with an accessibility relation ≤.

Given a sentence φ evaluated at a world G:

• G ⊨ ◇φ means: there exists H ≥ G with H ⊨ φ.

• G ⊨ □φ means: for all H ≥ G, H ⊨ φ.

The modal logic S4.2 is S4 (reflexive + transitive frames) plus the axiom:

\(\text{.2}\qquad \Diamond\Box p \to \Box\Diamond p.\)

A good mental picture: if your “future” is directed (any two futures can be merged), then .2 holds.

---

S4.2 is always valid

In our graph-minor frame:

• The relation ≤ is reflexive and transitive (minors compose).

• The frame is directed: given graphs G and H, the disjoint union G ⊔ H is a common extension, because both G and H are minors of G ⊔ H (delete the other component).

  

Directedness implies the modal axiom .2, hence S4.2 is valid in the frame.

So we already have the lower bound:

\(S4.2 \subseteq \text{Validities of our graph-minor system}.\)

The real work is showing the upper bound: nothing strictly stronger than S4.2 is valid.

---

Buttons and switches

This is the core method. It originates with Hamkins–Löwe in the forcing context, and the general “structural connections/control statements” framework was developed further by Hamkins–Leibman–Löwe in the context of a forcing class. We use the Kripke‑model formulation as stated (and applied) in Hamkins–Linnebo, Theorem 5, although the underlying control‑statement method is due to the earlier papers.

Buttons

Following Hamkins–Löwe, a sentence b is a button if it is pushable from anywhere: □◇□b.

Intuitively: no matter where you are, you can move to an extension where b becomes permanently true.

A button b is a pure button if it is also persistent upward: □(b → □b).

In that case, once b ever becomes true, it remains true in all further extensions.

A finite family {b₀, …, bₘ₋₁} is independent if, from any world where some of them are still false, you can push any chosen unpushed button bᵢ without accidentally pushing any other still‑unpushed bⱼ.

Switches

Following Hamkins–Löwe, a sentence s is a switch if it is toggleable from anywhere: □◇s ∧ □◇¬s.

A finite family {s₀, …, sₖ₋₁} of switches is independent if, from any world, you can reach an extension realizing any chosen truth pattern for s₀, …, sₖ₋₁.

The key theorem

Hamkins–Löwe prove a general “control statements” result:

The key theorem (control statements ⇒ S4.2 upper bound).
If, at some world W, you have arbitrarily large finite families of independent buttons and switches, with the chosen buttons not yet pushed at W, then the propositional modal validities at W (under the allowed substitutions) are contained in S4.2.

So the upper bound reduces to building (i) many independent first‑order buttons and (ii) arbitrarily large finite families of independent first‑order switches, and checking that switch moves don’t interfere with buttons and vice versa.

---

Buttons in the graph-minor world: spiders

The spider graphs S(a,b,c)

Fix integers a, b, c ≥ 1. Let S(a, b, c) be the 3-legged spider:

• one center vertex of degree 3,

• three internally disjoint paths (legs) of lengths a, b, c starting at the center.

These are finite trees of maximum degree 3.

The button sentence β(a,b,c) is first-order in {E}

Let β(a,b,c) be the parameter-free first-order sentence:

“There exist distinct vertices forming a subgraph isomorphic to S(a,b,c).”

Concretely: you existentially quantify the center vertex and the vertices along each leg, assert all are distinct, and assert the edges along the three paths. This uses only E(x,y) and equality.

Clarification. In the spider buttons β(a,b,c), “subgraph” means not necessarily an induced subgraph. Equivalently, β(a,b,c) is an existential {E}-sentence asserting the presence of the required spider edges but not forbidding additional edges among the witnessing vertices. This is the appropriate notion here, since extensions (minor-extensions) may add edges, which would destroy induced subgraphs but not ordinary subgraphs.

Why this is actually a button

The minor relation is not “subgraph extension,” so “contains a given finite subgraph” is not generally persistent.

The trick is a standard theorem from graph minor theory:

Subcubic minor ⇒ topological minor.
If a finite graph H has maximum degree at most 3 and H is a minor of G, then G contains a subdivision of H as a subgraph. That is, after replacing some edges of H by paths, one can find the resulting graph sitting directly inside G. (Reference: S. Norin, Graph Minors notes, Lemma 1.3.)

Finite‑ambient reduction (since our worlds may be infinite).
Norin’s Lemma 1.3 is stated for finite graphs. That’s enough for us: if a finite graph H is a minor of an (even infinite) graph G, then H is already a minor of some finite subgraph G₀ ⊆ G.

Reason: in a branch‑set minor model of a finite H in G, only finitely many branch sets and finitely many edges witnessing adjacencies are involved; connectivity inside each branch set is witnessed by finitely many finite paths. Taking the finite union of these witnesses gives a finite G₀ carrying the same minor model.

So we may apply Norin’s lemma to G₀, and hence to G.

Apply Subcubic minor ⇒ topological minor with H = S(a,b,c). Any subdivision of a spider still contains the original spider as a subgraph: each subdivided leg is just a longer path, so by truncating each leg to its first a, b, and c edges from the center, we recover an actual copy of the original spider.

We therefore obtain the crucial equivalence:

G ⊨ β(a,b,c) ⇔ S(a,b,c) ≤ G.

From this, persistence is immediate:

• if β(a,b,c) holds at G, then S(a,b,c) ≤ G;

• for any extension H ≥ G, transitivity of the minor relation gives S(a,b,c) ≤ H;

• hence β(a,b,c) holds at H.

Pushability is also immediate: from any graph G, the extension G ⊔ S(a,b,c) makes β(a,b,c) true.

Therefore each β(a,b,c) is a pure button: once it becomes true, it remains true in all further extensions.

---

Many independent buttons: equal-size, non-isomorphic spiders

To obtain many independent buttons, we choose spiders that satisfy two conditions:

• they all have the same number of vertices, and

• they are pairwise non-isomorphic.

Fix a large integer N and choose many distinct triples

1 ≤ aᵢ ≤ bᵢ ≤ cᵢ
aᵢ + bᵢ + cᵢ = N.

The sorting aᵢ ≤ bᵢ ≤ cᵢ matters: it ensures that we are not accidentally choosing the same spider with permuted leg labels.

Let βᵢ = β(aᵢ, bᵢ, cᵢ) and Sᵢ = S(aᵢ, bᵢ, cᵢ). All Sᵢ have N + 1 vertices.

Dynamic independence: pushing one spider doesn’t push the others

Suppose you are at some world U where certain buttons βᵢ are still false. To push a particular button βᵢ, move to the extension

U′ = U ⊔ Sᵢ.

In U′, the button βᵢ is now true.

Could this operation accidentally make some other button βⱼ (with j ≠ i) become true as well? That would mean that the spider Sⱼ has become a minor of U′.

But Sⱼ is connected, and any connected minor must be realized inside a single connected component. Therefore Sⱼ would have to be a minor of the new component Sᵢ. (Formally, in a branch‑set minor model of a connected graph, the branch sets are connected and linked by edges witnessing adjacencies, so they must all lie inside a single connected component of the ambient graph.)

At this point we use a simple branch-set counting lemma.

Lemma (same-size connected minor of a tree is isomorphic).
If T is a finite tree and H is a connected minor of T with the same number of vertices, then H must in fact be the same tree: H ≅ T.

Reason: in a branch-set minor model, |V(H)| disjoint nonempty branch sets must fit inside |V(T)| vertices. Therefore each branch set must consist of exactly one vertex. It follows that H is a spanning subgraph of T.

But a spanning subgraph of a tree is connected if and only if it contains all edges of the tree. Hence H must in fact be the whole tree, and so H ≅ T.

Since Sᵢ and Sⱼ have the same number of vertices but are not isomorphic, Sⱼ cannot be a minor of Sᵢ. Therefore pushing βᵢ cannot accidentally push any other βⱼ.

Conclusion: at the base world K₁ (a single isolated vertex), we have arbitrarily large finite independent families of first-order buttons.

---

Switches in the graph-minor world: prime cycle components

This is the part AI tends to mess up unless you insist on “toggleability” and “independence” checks.

The FO sentences σₚ: “there is a component exactly Cₚ”

Fix an odd prime p ≥ 5. Let σₚ be the parameter-free first-order sentence (in the graph language with just the edge relation E):

“There exists a connected component isomorphic to the cycle Cₚ.”

This is first-order because p is fixed: you quantify p distinct vertices, assert that they form a cycle, and assert there are no extra edges among those vertices besides the cycle edges.

A chord of a cycle is an extra edge connecting two non-consecutive vertices on that cycle. So “no chords” means the only edges among those p vertices are the p cycle edges.

Finally, you assert that none of these vertices has a neighbor outside the set (so they form an entire connected component).

Now pick distinct primes
p₀ < p₁ < ⋯ < pₖ₋₁
and write σⱼ = σₚⱼ.

Why each σₚ is a switch

Turn on: from any graph G, the extension G ⊔ Cₚ satisfies σₚ.

Turn off: from any graph G, subdivide every edge in every connected component of G that is exactly Cₚ. Each such component becomes C₂ₚ, so σₚ becomes false.

To justify that subdividing even infinitely many edges still gives an extension (in the minor preorder), we use an explicit branch‑set model.

Lemma (subdivide any set of edges ⇒ minor extension).
If H is obtained from G by subdividing an arbitrary set of edges (possibly infinite), then G ≤ H.

Sketch: well-order V(G) (Choice). For each subdivided edge uv with new vertex w(uv), assign w(uv) to the branch set of min(u,v). Then every original edge is witnessed either by the unchanged edge, or by the second half of the subdivided path.

Independence (arbitrarily many switches).
Pick distinct odd primes p₀ < p₁ < ⋯ < pₖ₋₁ and consider σ₀, …, σₖ₋₁. From any world G and any target pattern S ⊆ {0,…,k−1}, first turn off σⱼ for every j ∉ S by subdividing every edge in every component that is exactly the cycle of length pⱼ. Then turn on σⱼ for every j ∈ S (if needed) by taking disjoint union with a fresh cycle of length pⱼ.

Because 2pⱼ is even, it cannot equal any odd prime pⱼ′, so turning off one σⱼ cannot accidentally turn on another σⱼ′. Thus {σ₀,…,σₖ₋₁} is an independent family of switches, and as k grows we get arbitrarily large finite families.

Remark (J. D. Hamkins). As Joel David Hamkins observed in the comment section, one can also turn off the cycle-component switches in a simpler way—for example, by attaching a single pendant edge (“twig”) to a Cₚ-component, or by adding a hub vertex to make it a wheel—thereby destroying the property of being a Cₚ-component. These alternative moves avoid any need to assume that p is prime. We use the edge-subdivision method Cₚ ↦ C₂ₚ (with a fixed finite set of chosen primes p) only because it keeps the modified components of maximum degree ≤ 2, which makes independence from the spider buttons immediate via a degree argument, and because 2p is never among the chosen primes.

---

Buttons and switches don’t interfere

Switch operations only affect cycle-like components, which have maximum degree at most 2. To make the “no spiders appear” argument precise in the branch-set setting, we use the following lemma.

Lemma (branch-set version).
If Δ(G) ≤ 2 and H ≤ G, then Δ(H) ≤ 2.

Proof idea.
Fix a branch-set minor model μ of H in G, and let X = μ(v). Since Δ(G) ≤ 2, every connected component of G is a path or a cycle (finite or infinite), and X lies inside one such component.

The edge boundary δ(X) — the set of edges with one endpoint in X and the other outside — has size at most 2. Each distinct neighbor of v in the minor H requires a distinct boundary edge leaving X, so the degree of v in H is at most 2.

Since v was arbitrary, Δ(H) ≤ 2.

It follows that switch moves cannot create a spider minor (spiders have a vertex of degree 3). Conversely, pushing a spider button adds a tree component, which cannot create or destroy prime cycle components. Therefore pushing buttons does not affect the switches.

Thus buttons and switches are independent.

---

Final step: exact modal validities are S4.2

We now have two bounds.

• Lower bound: the frame is directed, so S4.2 is valid at every world.

• Upper bound: at K₁ we have arbitrarily large finite families of independent first‑order buttons and switches, with the chosen buttons not yet pushed at K₁. By the Hamkins–Löwe control‑statement theorem, the propositional modal validities at K₁ are contained in S4.2.

Putting these together gives:

Val(K₁) = S4.2.

And since K₁ is a world in the frame, any modal principle not in S4.2 already fails at K₁, so it cannot be globally valid. Therefore the global validities of the entire graph-minor system are exactly S4.2.

---

The part you don’t see in the final proof: the proof‑debugging loop

The final argument looks smooth. It absolutely did not appear smooth on the first try.

The way I got there was:

• ask the AI for a full solution;

• ask it to find mistakes;

• fix the specification / patch lemmas;

• ask it again to find remaining mistakes;

• repeat until nothing breaks.

That “find mistakes → apply fixes” loop wasn’t cosmetic. It was mathematically necessary, because the problem has a lot of interacting constraints:

• worlds include infinite graphs;

• ≤ is minor, not “subgraph extension”;

• substitutions must be parameter‑free first‑order in the single relation symbol E;

• buttons must be persistent under minor extensions;

• independence must be dynamic (not just “there exists a world with this pattern”);

• switches must genuinely be toggleable (□◇s and □◇¬s) and independent;

• buttons and switches must not interfere.

An AI draft can satisfy 90% of that and still be wrong.

What follows is the story of the main failures and how I fixed them — written as a practical guide to “how to use AI for math without fooling yourself.”

---

Failure 1: “A button is ‘contains a fixed finite subgraph’”

The AI’s first reflex was the obvious one:

• propose a button b_F = “this graph contains F as a subgraph.”

• to push it: go to G ⊔ F.

• claim persistence: once F appears, it stays.

What went wrong: persistence is false under minors.

Minor extensions are not subgraph extensions. You can extend a graph by subdividing edges, which often destroys exact finite subgraph patterns. The triangle example is the classic: subdivide one edge of a triangle and you kill triangles as subgraphs, even though the triangle still exists as a minor.

Fix: stop trying to make “contains F as a subgraph” be persistent. Under minors it usually isn’t.

Meta‑lesson: whenever the AI asserts persistence, force it to produce a counterexample or a theorem. “Seems obvious” is not a proof.

---

Failure 2: “Use trees as buttons” (still not persistent)

Next attempt: “fine, triangles are fragile; use trees.”

Same problem: for many trees T, “contains T as a subgraph” is still not upward‑persistent under minors, because a tree can appear as a minor via a subdivision‑type model without appearing as an exact subgraph copy.

Fix: we needed a gadget where “minor ⇒ subgraph copy” can be made true.

---

The key pivot that worked: subcubic minor ⇒ topological minor

At this point we moved from ad‑hoc gadget hacking to the right bit of graph minor theory:

Subcubic minor ⇒ topological minor.
If H is finite and has maximum degree ≤ 3, and H is a minor of G, then G contains a subdivision of H as a subgraph.
(We cited S. Norin’s graph minors notes, Lemma 1.3.)

This is the right bridge because it turns a “minor fact” (hard to express in FO) into a “subgraph existence fact” (easy to express in FO).

But the AI made a predictable mistake next…

---

Failure 3: “Subdivision of H exists ⇒ H exists as a subgraph”

The theorem gives: “a subdivision of H appears as a subgraph.”

The AI silently upgraded that to: “so H itself appears as a subgraph.”

That’s not true in general.

Fix: choose H so that every subdivision of H still contains H as a subgraph.

We did this by choosing H to be a 3‑leg spider S(a,b,c):

• one center of degree 3;

• three internally disjoint legs (paths) of lengths a, b, c.

Any subdivision of a spider just lengthens legs. You can literally “truncate” each leg back down to length a, b, c and recover the original spider as a subgraph.

That gives the crucial equivalence:

\(G \models \beta(a,b,c) \;\Longleftrightarrow\; S(a,b,c) \leq G .\)

Here β(a,b,c) is the FO sentence “there exist vertices forming a subgraph isomorphic to S(a,b,c).”

From that, persistence becomes immediate: if β holds at G, it holds at all H ≥ G.

Meta‑lesson: AI often applies a correct theorem and then adds an extra implication it didn’t justify. The fix is usually to narrow the gadget until the “extra implication” becomes actually true.

---

Failure 4: Independence was proven in the wrong sense

After buttons existed, the AI tried to conclude “so we get S4.2.”

But the Hamkins–Löwe control‑statements theorem doesn’t just want “many buttons exist.” It wants independent buttons in a dynamic sense:

From any world, you can push any chosen unpushed button without accidentally pushing any other still‑unpushed buttons.

The AI initially gave only a static pattern argument (“for every subset B there exists a world where exactly those hold”), which is not enough.

Fix: prove dynamic independence properly.

The proof used two small but decisive facts:

• Connected minors live inside one connected component.
  In a branch‑set minor model, branch sets are connected and linked by witnessing edges, so a connected minor can’t “use multiple components.”

• Same‑size connected minor of a tree is isomorphic (branch‑set counting).
  If T is a finite tree and H is connected with H ≤ T and ∣V(H)∣ = ∣V(T)∣, then every branch set must be a singleton, so H is a spanning subgraph of T. A spanning subgraph of a tree is connected iff it contains all edges, so H ≅ T.

Then pushing βᵢ by adding a new component Sᵢ cannot accidentally push βⱼ: if Sⱼ became a minor, it would have to appear as a connected minor of Sᵢ, but “same size + connected + tree” forces isomorphism.

Meta‑lesson: AI will happily “prove independence” using the wrong definition unless you force it to match the theorem’s hypothesis word‑for‑word.

---

Failure 5: The first “switches” weren’t actually switches

The switch stage is where AI often fails in the simplest way: it writes down a family of sentences and calls them “switches,” without checking □◇s and □◇¬s.

A typical first attempt was to use something monotone, like:

• “G has Cₚ as a minor,” or even

• “G contains Cₚ as a subgraph,”

and then to claim “we can always turn it off later.”

What went wrong: monotone properties aren’t switches. If s is upward‑persistent (□(s → □s)), then once s becomes true you can never reach ¬s, so □◇¬s fails. Even when the property isn’t literally monotone, “turn it off” can fail globally because you might not have any way to destroy all witnesses without breaking the extension relation.

Fix: pick a genuinely toggleable gadget. We used:

• σₚ = “there exists a connected component isomorphic to the cycle Cₚ.”

Then:

• Turn on: from any G, go to G ⊔ Cₚ.

• Turn off: subdivide every edge in every component that is exactly Cₚ, turning each such component into C₂ₚ, so σₚ becomes false.

Independence then comes from choosing distinct odd primes p₀ < … < pₖ₋₁: turning off σₚⱼ produces an even cycle length 2pⱼ, which cannot accidentally turn on any σₚⱼ′.

Meta‑lesson: switches have two unit tests: (1) toggleability (□◇s and □◇¬s) and (2) independence (you can realize any finite truth pattern without disturbing the other switches). Make the AI check both explicitly. If it can’t, your “switches” are probably fake.

---

Failure 6: Infinite graphs broke the “turn off” story unless we used branch‑set minors

Turning off σₚ means “destroy all Cₚ components,” which can involve infinitely many components.

The AI initially described this as doing infinitely many contractions later, which is not a definition.

Fix: switch fully to the branch‑set definition for infinite minors and give an explicit branch‑set model showing:

If H is obtained from G by subdividing any set of edges (even infinitely many), then G ≤ H.

We used Choice to well‑order V(G), then assigned each new subdivision vertex w_uv to the branch set of min(u,v). That gives a clean minor model.

This matters because in infinite settings, you don’t want “procedural” arguments (“do infinitely many contractions”). You want “there exists a branch‑set model,” because that’s the actual definition.

Meta‑lesson: in infinite combinatorics, always force the AI to argue in the language of the definition, not in the language of operations.

---

Failure 7: “Degree ≤ 2 is minor‑closed” proof had a subtle bug

To show the switches don’t accidentally create spider buttons, we used:

• switch operations only touch cycle‑like components (max degree 2),

• spiders require a degree‑3 vertex,

• so switch moves can’t create spider minors.

But the AI’s first branch‑set proof of “Δ ≤ 2 is minor‑closed” had a subtle error in the singleton branch‑set case.

Fix: rewrite using the correct invariant: the edge boundary δ(X) of a connected branch set X in a path/cycle has size ≤ 2, even when X is a single vertex. Each neighbor in the minor needs a distinct boundary edge, so degree stays ≤ 2.

Meta‑lesson: this is exactly why “ask AI to find remaining mistakes” is powerful: it forces the assistant into adversarial mode where small landmines actually get noticed.

---

Why this workflow works (and when to stop iterating)

The whole point of the “find mistakes → apply fixes” loop is that it turns a proof into something you can unit test.

Every time I asked “find remaining mistakes,” I was really asking the AI to run a test suite:

• Is the supposed button actually persistent under minors?

• Are the FO sentences really parameter‑free in the language with only E?

• Are the supposed switches actually switches (□◇s and □◇¬s)?

• Are the switches independent (can we realize any finite truth pattern without disturbing the others)?

• Does the infinite case secretly rely on finite operations?

• Did we use the correct definition of independence?

• Did we accidentally pick isomorphic spiders by permuting legs?

The moment the AI can’t find a counterexample, and every constraint has an explicit lemma (or citation), you stop iterating and write the clean narrative.

But note the human role: you have to make informed decisions when the AI exposes ambiguity. In our conversation, we repeatedly pinned down the spec:

• “All simple graphs, including infinite.”

• “Use branch‑set minors.”

• “No restriction to finite operations.”

• “Parameter‑free FO sentences only.”

• “Assume Choice.”

Those aren’t cosmetic. They determine what counts as a valid proof step.

That’s why the workflow converges: not because the AI magically gets reliable, but because we gradually eliminate underspecified degrees of freedom until the only remaining path is the correct one.

---

The punchline

After this debugging process, we ended up with:

• a family of pure FO buttons β(a,b,c) from spiders, using the cited subcubic‑minor theorem plus truncation;

• arbitrarily large finite families of them that are dynamically independent (same‑size connected minor of a tree forces isomorphism);

• arbitrarily large finite families of independent FO switches σₚ from prime cycle components, toggleable via subdivisions and disjoint unions;

• a precise non‑interference proof using a branch‑set “Δ ≤ 2 is minor‑closed” lemma;

• and then the Hamkins–Löwe/Hamkins–Linnebo control‑statements theorem gives the S4.2 upper bound, matching the directedness lower bound.

So the exact propositional modal validities of the graph‑minor Kripke model (under parameter‑free FO(E) substitutions) really are S4.2.

And the bigger takeaway is methodological: AI can be excellent at generating candidate structures, but it needs to be forced through the same adversarial proof‑hygiene process you’d use with a human collaborator — otherwise you’ll get confident garbage.

The whole ChatGPT 5.2 Pro conversation on which this article is based on this conversation. (Note that the conversation uses dials, whereas in my exposition I used switches instead.)

---

References

• S. Norin, Graph Minors notes (especially Lemma 1.3: subcubic minor ⇒ subdivision/topological minor).

• J. D. Hamkins & B. Löwe, The modal logic of forcing

• J. D. Hamkins & Ø. Linnebo, The modal logic of set-theoretic potentialism and the potentialist maximality principles

• J. D. Hamkins & G. Leibman & B. Löwe, Structural connections between a forcing class and its modal logic