Applied Case: The Mathematician Still Has a Job

Yesterday I published Conjecture 8 with the rest of the handoff attached.

Applied Case: I Gave a Mathematician Homework

Introducing Proof-to-Theory

Modal Path EthicsAidan Lawson

The proof was there. The machine was there. The counterfactuals were there. The reader could press the buttons, follow the histories, open the mathematical reference, and check which part of the explanation was doing which job.

Proof-to-Theory started to cleanup that handoff.

Today, Chair44 handed me a cleaner test.

• The result had already been found.
• The proof had already been written.
• The proof had already been formalized.
• And mathematicians were still trying to make it understandable.

Perfect.

We have a benchmark.

The Chair.

Chair44 is a proposed three-dimensional aperiodic monotile from Ioannis Tsiokos.

Start with the ordinary three-dimensional chair: a 2×2×2 cube with one corner removed, leaving seven unit cubes.

Now decorate its exposed square faces with tiny geometric features. Those features constrain which copies of the chair can physically meet.

Tsiokos's September 16 preprint claims that one resulting shape, Chair44, tiles three-dimensional Euclidean space, but every complete tiling by congruent copies lacks a translational period. The paper claims more than that: every tiling is homochiral, carries a unique infinite hierarchy of nested supertiles, and has a symmetry group of order at most twenty-four.

You can kill ordinary translation and still leave an infinite screw symmetry alive. Strong aperiodicity has to close that route too.

The paper presents Chair44 as a proof submission. It combines geometric arguments, exhaustive finite checks, and a Lean formalization. The construction itself was found with GPT-6 Astra. Tsiokos told Quanta that "The 3D Einstein was found by Astra, not me," and said that he understood the intuitive geometric argument rather than the full mathematics.

That is another handoff problem. The theorem does not become easy to understand when the proof becomes available.

The Rule Comes Back

Eight chairs fit together into a larger chair.

That alone is not enough. Lots of shapes can be assembled into larger copies of themselves without forcing an aperiodic universe.

The important part is that the contact rule survives the move upward.

The small chairs are forced into one unique eight-chair parent. The allowed contacts between those parents, after rescaling by one half, obey the same allowed contact language as the original tiles.

The rule comes back.

Call the coarsening operation D. If a tiling T had a translational period p, then the coarsened tiling D(T) would have period p/2.

Coarsen again.

p/4.

Again.

p/8.

Every level remains registered on the same kind of discrete lattice. A nonzero lattice vector cannot stay divisible by every power of two.

The period runs out of places to go.

That is the piece of Chair44 a human being can carry.

Unfortunately, getting to that sentence requires proving that the physical shape really forces the registered contact language, that every tile has one unique parent, that parent contacts really close back into the same language, and that the physical construction can be iterated without quietly switching to a different abstract problem.

Then the full strong-aperiodicity claim still needs the orientation argument. The source restricts the possible proper cubic frames to twenty-four. Once the translation kernel is gone, an ambient symmetry is determined by its frame, so the whole symmetry group is finite.

The short explanation is short because the long proof did its job first.

PTT-041

So Modal Path Ethics turned Chair44 into a blind Proof-to-Theory benchmark.

The worker received the original Tsiokos paper and the exact pinned proof repository. It did not receive Chaim Goodman-Strauss's later note, the forum discussions, or the later simplified explanations.

Then we let it reconstruct what the proof was carrying.

The result was frozen before comparison.

The ruling was:

MECHANISM: PASS

REPRESENTATION: PARTIAL

That split is the important result.

Proof-to-Theory recovered the physical registration gateway, the forty-four-contact language, the unique eight-child parent recognizer, self-closed coarsening, period halving, and the separate twenty-four-frame symmetry argument.

Its compact dependency chain was essentially:

• physical geometry
  • → registered contacts
    • → unique parent
      • → same rule after coarsening
        • → period halving
          • → finite symmetry

That is very close to the mathematical engine a person needs.

Then the system stopped pretending.

The source still contained thousands of finite geometric and recognizer obligations. Proof-to-Theory could explain what those checks established. It could compress them into an interface. It could not produce a small, human-derived reason that made the finite census visually obvious.

Its own frozen report said the remaining debt was a "small, checkable diagram or invariant" that would make the collision and parent-recognition structure conceptually evident.

Then, we opened Goodman-Strauss.

Three Colors

Chaim Goodman-Strauss posted Notes on a strongly aperiodic monotile in E³ five days after the original preprint.

The abstract is one sentence.

"We provide a clearer presentation of the Chair44 monotile."

Goodman-Strauss redraws the matching information on the three-dimensional L-shaped chair using three kinds of markings.

• Red.
• Green.
• Blue.
  • Red meets green.
  • Green meets red.
  • Blue meets blue.

Now build the eight-chair supertile. The markings inherited by the supertile reproduce the same kind of matching information carried by one tile. The parent therefore fits to neighboring parents in the same way the child fits to neighboring children. The recursion is visible.

• Proof-to-Theory had found the engine.
• Goodman-Strauss found the representation in which the engine becomes easy to see.

That is a better result than having one of them "win."

The machine did not eliminate the mathematician. It located the part of the proof where the mathematician was still most valuable.

Unfortunately, Mathematicians Have Forums

Then I opened the forums.

This was a mistake in exactly the same sense that opening Smogon Policy Review is a mistake.

Within minutes, the argument was no longer only about whether the tile works.

It was about whether the original paper explained itself properly, whether a formal proof can compensate for bad exposition, how much credit belongs to the person who prompted the model, whether the model "found" the object, whether a cleaner human proof changes the status of the original result, and whether any of this is how mathematics is supposed to arrive.

I have seen this institution before.

Create-A-Pokémon can spend six weeks arguing about whether a move belongs on a fictional moth because the move is carrying an actual question about the metagame.

Mathematicians can spend six days arguing about a badly explained monotile because the explanation is carrying an actual question about mathematical authority.

The object can be valid while the handoff is bad. The handoff can be improved without becoming the discovery. A formal certificate can establish something while leaving the community without a representation it can think with. A cleaner representation can become the thing everybody remembers without retroactively doing the finite verification work that made it safe to trust.

These are different offices.

The forum drama is what happens when everybody starts litigating the jurisdiction between them.

I regret to report that mathematicians are Smogon users with grants.

The First External Test

Chair44 is the first clean external calibration of Proof-to-Theory. It did not prove that Proof-to-Theory can replace mathematical exposition. It gave us something more specific.

Proof-to-Theory can take a large, heterogeneous proof package and recover a source-bound map of where the theorem actually lives.

It can preserve distinctions that a fluent summary likes to erase.

Physical shape versus abstract matching rule. Existence versus universal structure. No translations versus full strong aperiodicity. A mechanism that has been recovered versus a representation that still has to be invented. And, at least in this case, it can identify its own representation debt before seeing the human answer.

That last point matters most.

The frozen report did not know that Goodman-Strauss was going to arrive with red, green, and blue. It knew that somebody still needed to arrive with something like that. That is its job.

Yesterday's article asked what comes after the proof.

Chair44 gives one answer.

Sometimes what comes after the proof is a mathematician drawing three colors on the thing and suddenly everybody can see it.

I would like Proof-to-Theory to help get that mathematician to the right page faster.

What Happens Next

Chair44 was retrospective.

The human simplification already existed. I hid it, ran the translation, froze the answer, and compared afterward.

The next tests are prospective.

Proof-to-Theory is now being run against live machine mathematics before the field has settled on its preferred explanation.

The standard gets harder from here.

A useful system should not only tell us what a proof means after somebody else has already found the right picture. It should preserve enough of the proof, expose enough of the mechanism, and localize the remaining debt well enough that the next human or machine researcher can do better work from there.

That is why the target is not "replace Goodman-Strauss."

The target is:

Get Goodman-Strauss to the three colors sooner.

The proof was already there.

The theory was still arriving.

Chair44, From Proof to Theory

Download the exact frozen PTT-041 candidate.

Sources

1. Ioannis Tsiokos, "A Strongly Aperiodic Monotile in Three Dimensions," arXiv:2609.19214, submitted September 16, 2026.

https://arxiv.org/abs/2609.19214

2. Chaim Goodman-Strauss, "Notes on a strongly aperiodic monotile in E³," arXiv:2609.24779, submitted September 21, 2026.

https://arxiv.org/abs/2609.24779

3. Konstantin Kakaes, Quanta Magazine, "Transformation" update on Chair44, September 2026.

https://www.quantamagazine.org/updates/transformation/

Status note. Tsiokos presents Chair44 as a proof submission. This article reports the source claim, the frozen PTT-041 reconstruction, and the later comparison to Goodman-Strauss. It is not an independent verification of the Chair44 theorem.