Michael Schroeder · Preprint · Version 1.0 · 3 October 2026 · ORCID 0009-0004-3249-0195

A Universal Turing Machine with 20 Instructions

DOI: 10.5281/zenodo.23095173

Abstract

We construct a universal Turing machine with five states, five symbols and 20 instructions in the standard model: one bi-infinite tape, left and right moves only, finite input on a blank background, and halting at an undefined transition. This improves on our earlier 21-instruction machine and other known machines in this model by Rogozhin and by Neary and Woods which use 22. The saving comes from a redesigned printing and restoration protocol that exploits a parity invariant. A direct compiler, with no intermediate tag system, drives the machine through a queue of unary addresses, periodically rebuilding its program so that the history it traverses stays short. It simulates a fixed source machine halting after t steps on input of length n in O((t+1)(n+t+1)2) time and O((t+1)(n+t+1)) space. For n = O(t) this is cubic time, though the constants are astronomically large. Lean 4 proofs establish universality, halting equivalence, these bounds, and recovery of the source machine's final configuration.

Paper and Supplement

The paper presents the 20-instruction machine, direct compilation with self-refresh, resource bounds and recovery of the source machine’s final configuration. The supplement supplies detailed proofs, exact costs, compiler optimisations and independent verification evidence.

Lean Proofs and Verification Materials

The complete release includes both PDFs and their LaTeX sources, the Lean 4 development, the frozen formal companion, independent Python simulators and compiler checks, concrete queue replays, verification records and integrity checksums.

Start with START_HERE.txt in the archive and run python3 verify_bundle.py to check the delivered files. The guide gives the steps for a cache-free Lean build and independent compiler, queue-replay and readback checks. Reproduction requires Python 3.10+ and Lean 4.32.2, with no external Lean packages. Use a fresh extraction for reproduction so the archived verification records remain intact.

Citation and file integrity

Schroeder, Michael. A Universal Turing Machine with 20 Instructions. Version 1.0, Zenodo, 2026. DOI: 10.5281/zenodo.23095173. Download the BibTeX citation.

The paper, supplement and ZIP on this site are byte-identical to the published Zenodo files. Download the SHA-256 checksums. The archive contains its own manifests and verification record.

The unchanged archive preserves preparation-time notes about the Zenodo draft. The Version 1.0 record linked here was published on 3 October 2026.

The Result and Its Formalization

The machine has five states, five tape symbols and 20 defined instructions. It uses one head on one bi-infinite tape, starts from finite input on a uniform blank background and halts at an undefined transition. A parity invariant underlies the instruction saving from the earlier U21 construction. A direct compiler uses a queue of unary addresses and periodically rebuilds the program beside its live data.

For a fixed source machine halting after t steps on input of length n, the target uses O((t+1)(n+t+1)2) time and O((t+1)(n+t+1)) space. When n = O(t), these are cubic time and quadratic space. The fixed-source constants are astronomically large; these are asymptotic simulation bounds.

Lean 4 verifies the transition table and instruction count, finite-input universality, halting equivalence, the time and whole-trace space bounds, and recovery of the source’s final state, head position and tape. The compiler requires no advance bound on future source runtime or tape use. Independent compressed queue replays check two complete reference examples; these are distinct from instruction-by-instruction target runs.

Licenses

The paper and technical supplement, including their LaTeX sources and original figures, are licensed under CC BY 4.0. The original Lean and Python code and associated software documentation and verification data are licensed under the MIT License. The archive’s LICENSE.txt, LICENSE_SCOPE.json and LICENSES/ specify the separate scopes and preserve third-party notices.

Acknowledgments

The construction builds on Neary and Woods’ small-machine architecture and the preceding U21 development. AI-assisted tools were used in the development and preparation of the paper. The Lean companion and independent execution checks provide the stated evidence; responsibility for the manuscript and its claims remains with the author.