Section 2 will formally describe details of a particular Gödel machine, focusing on its novel aspects, skipping over well-known standard issues treated by any proof theory textbook. Section 2.2.1 will introduce the essential instructions invoked by proof techniques to compute axioms and theorems and to achieve goals, thus relating syntax to semantics. Section 2.2.2 will elaborate on the above-mentioned Global Optimality Theorem 2.1. Section 2.3 will describe the conceptually separate BIOPS initialization and its asymptotic optimality properties. Section 3 will discuss the Gödel machine's limitations, possible types of self-improvements, and additional differences from previous work. Section 4 will summarize.