# tkmt-lab — research lab of Tatsuhiko Takimoto

> Independent research in mathematics and science with AI teams. The first results are on fullerene graphs. Each result is released with a paper, a Lean 4 formalization where available, verification data, and a machine-readable claim list stating what has and has not been checked.

## Works

- [A3 classification of linear gSW paths](https://github.com/tkmt-lab/a3-gsw-classification): GC(k,l)[C20] has a literal linear generalized Stone-Wales path iff an explicit two-stage residue criterion holds. Proved in Lean 4 (standard axioms only), checked with Comparator against an independent statement. Start with AGENTS.md; evidence in packet/claims.json. Current release: tag v1.0.5; Zenodo doi:10.5281/zenodo.23491202 (all versions).
- [Eventual periodicity on affine rays](https://github.com/tkmt-lab/gsw-ray-periodicity): for fullerene families built from a fixed number of convex lattice faces with affine coordinates, existence of a literal gSW path is eventually periodic along every integer affine ray. Main theorem proved in Lean 4 (standard axioms only) for a specification with weaker hypotheses than the paper, checked with Comparator; a prose lemma connects the paper's geometric hypotheses to it. For Graver's family K3(r,s) (two caps of four triangles of side r joined by three hexagons with sides r, r, s, r, r, s) the result on every ray in r, s ≥ 1 and the closed classification (for r, s ≥ 2: a path exists iff s ≡ ±1 mod r) are Lean-proved with no prose step; the same holds for Graver's family C1 (for a, b ≥ 1: a path exists iff b = 1), for Graver's family O2 the ray result and absence of paths for t, d ≥ 2 are Lean-proved with no prose step, and so are the ray result for Graver's family D14 and the classification (r ≥ 2) and ray result for Graver's family E10. Lean also covers the family arithmetic. Start with AGENTS.md. Current release: see the repository's releases; Zenodo doi:10.5281/zenodo.23491204 (all versions).

## Built on

- The question: linear generalized Stone–Wales paths as defined by A. Bille, V. Buchstaber and E. Spodarev ("Some open mathematical problems on fullerenes", 2024/2025).
- The Goldberg–Coxeter construction (named after M. Goldberg and H. S. M. Coxeter; developed for plane graphs, with zigzag theory, by M. Dutour Sikirić and M. Deza).
- J. E. Graver's catalogue of fullerenes with ten or more symmetries; K. Kutnar and D. Marušič on cyclic edge-connectivity of fullerenes.
- The Büchi–Elgot–Trakhtenbrot theorem (monadic second-order logic on words and finite automata).
- Lean 4, mathlib, Comparator and independent Lean kernels.
- Full citations are in each paper.

## Other work

- Novelist: Tatsuhiko Takimoto (滝本竜彦), https://tatsuhikotakimoto.com/en/

## Evidence conventions

- Formal proof, independent derivation, AI review, and finite computation are labelled separately in each claims.json.
- Human peer review and novelty are not claimed unless stated.
- Contact: research@tatsuhikotakimoto.com, or GitHub issues in the relevant repository.
- News and the lab diary: https://x.com/tkmt_lab
- Licence of this site's text: CC BY 4.0. Each repository states its own licences.