Abstract: 
We formalize undecidablity results for Minsky machines. To
this end, we also formalize recursive inseparability.
We start by proving that Minsky machines can
compute arbitrary primitive recursive and recursive functions. We then
show that there is a deterministic Minsky machine with one argument
and two final states such that the set of inputs that are accepted in
one state is recursively inseparable from the set of inputs that are
accepted in the other state. As a corollary, the
set of Minsky configurations that reach the first state but not the
second recursively inseparable from the set of Minsky configurations
that reach the second state but not the first. In particular both
these sets are undecidable. We do
not prove that recursive functions can simulate
Minsky machines. 
BibTeX: 
@article{Minsky_MachinesAFP,
author = {Bertram Felgenhauer},
title = {Minsky Machines},
journal = {Archive of Formal Proofs},
month = aug,
year = 2018,
note = {\url{http://isaafp.org/entries/Minsky_Machines.html},
Formal proof development},
ISSN = {2150914x},
}
