tkmt-lab

Research lab of Tatsuhiko Takimoto · mathematics and science with AI teams

Reliable, careful research, done with respect for the researchers whose work we build on, and meant to contribute to society.

Works

Paper 1 · 2026

A two-stage classification of linear generalized Stone–Wales paths in Goldberg–Coxeter images of the dodecahedron

Which twisted football-shaped carbon cages have a straight path from pentagon to pentagon? Finding the rule, and proving it in Lean.

Fullerenes are cage-shaped carbon molecules made of pentagons and hexagons, like a football (C60 is the best known). The paths studied here are straight chains of hexagons running from one pentagon to another, along which a generalized Stone–Wales rearrangement of the cage acts. For one infinite family of twisted cages built from the dodecahedron, GC(k,l)[C20] with k > l > 0, we found a simple rule based on remainders that tells exactly which cages have such a path. Among the cages that are not just enlarged copies of a smaller one, the first without such a path has 7,980 carbon atoms.

Each square is one cage GC(k,l)[C20]. The colours follow the proved rule.

Paper (PDF) · Repository · doi:10.5281/zenodo.23491202 · claims.json · Build and axiom checks

The question is from the list of open problems on fullerenes by A. Bille, V. Buchstaber and E. Spodarev. The classification is proved in Lean 4 and checked with Comparator against a statement written in advance.

Paper 2 · 2026

Eventual periodicity of linear generalized Stone–Wales paths in affine fullerene families with convex lattice-face decompositions

Is there a rule that holds for whole families of fullerenes? Finding a general theorem, and proving it.

Paper 1 settles the question for one family. This paper proves a general theorem: for every fullerene family in a broad class (cages glued from a fixed number of flat lattice pieces whose sizes grow linearly), the answer to “is there such a path?” eventually repeats in a regular cycle as the cages grow. It applies at once to eleven families of Graver’s catalogue, so instead of checking cages one by one, one theorem covers infinitely many of them. A formal version of the theorem is proved in Lean. The proof shows that the cycle exists but in general does not compute it; for the families K3 and C1 the rule is explicit.

Graver’s family K3(5,s) for s = 2 to 41: a path exists exactly when s leaves remainder 1 or 4 on division by 5, so the pattern repeats every 5 steps.

Paper (PDF) · Repository · doi:10.5281/zenodo.23491204 · claims.json · Build and axiom checks

Extends the same question to the families of J. E. Graver's catalogue, using the classical link between monadic second-order logic and finite automata. A formal version of the main theorem is proved in Lean 4; it has weaker hypotheses than the paper, and a short prose lemma in the paper, not checked by Lean, carries the paper's geometric hypotheses to it. For the families K3 and C1 the whole chain, including their closed classifications, is Lean-proved with no prose step; for O2 the same holds for the ray result and the absence of paths when both parameters are at least 2, and for D14 for the ray result.

How the work is checked

Each release keeps different kinds of evidence apart, and says which applies to each claim:

Formal proof	Checked by the Lean 4 kernel. Separately, the Comparator tool checks that the proof proves exactly a statement written in advance by a different agent. Anyone can re-run the build; each repository's GitHub Actions workflow rebuilds the main modules and checks their axioms on every push. Any step from the paper to the formal statement that is not in Lean is said so in the repository.
Independent derivation	A second proof written by a separate team that did not see the first proof or its code.
AI review	Prose read and recalculated by an AI reviewer. Not human peer review.
Finite computation	Exhaustive or sampled checks, with their exact ranges.

What is not yet established — for example human peer review or novelty — is stated in each repository. Corrections are listed openly.

How this research is done

The research is carried out with AI systems (OpenAI Codex and Anthropic Claude Code) working as separate teams for exploration, independent verification, literature search and formalization. I, Tatsuhiko Takimoto, direct the work, make the decisions, and am responsible for what is released, its provenance and the stated limits of verification. AI systems are not listed as authors.

Built on the work of others

A. Bille, V. Buchstaber and E. Spodarev, who defined generalized Stone–Wales paths and collected open problems on fullerenes. Our question comes from their work.
M. Goldberg and H. S. M. Coxeter, after whom the Goldberg–Coxeter construction is named, and M. Dutour Sikirić and M. Deza, who developed it for plane graphs together with the theory of zigzags.
J. E. Graver, whose catalogue of highly symmetric fullerenes gives the families we study, and K. Kutnar and D. Marušič, whose work on cyclic edge-connectivity of fullerenes we rely on.
J. R. Büchi, C. C. Elgot and B. A. Trakhtenbrot, whose theorem connecting logic on words with finite automata is the last step of the periodicity proof.
The developers of Lean 4 and mathlib, and of the Comparator tool and the independent proof kernels used to check our proofs.

I am grateful to them, and I hope this work adds something new to the field they opened. The papers cite these and other sources in full.

For AI readers

A plain-text index is at llms.txt. Each repository has an AGENTS.md and a machine-readable claims.json.

My other work

Novelist: Tatsuhiko Takimoto (滝本竜彦)

Contact

Questions, errors and related work: research@tatsuhikotakimoto.com, or an issue in the relevant repository.

News and the lab diary: @tkmt_lab on X.

Licence

The text of this site is licensed under CC BY 4.0. Each repository states its own licences.