Abstract

We describe a proof by a computer program of the unsolvability of the halting problem. The halting problem is posed in a constructive, formal language. The computational paradigm formalized is Pure LISP, not Turing machines. The machine was led to the proof by the authors, who suggested certain function definitions and stated certain intermediate lemmas. The machine checked that every suggested definition was admissible and the machine proved the main theorem and every lemma. We believe this is the first instance of a machine checking that a given problem is not solvable by machine.