Followup to Fundamentals of Formalisation Level 5: Formal Proof. First post.

This is a new lesson of our online course on math formalizations required for AI safety research.

The big ideas:

Turing Machine
The Halting Problem

To move to the next level you need to be able to:

Describe a turing machine and write basic turing algorithms.
Give the basic idea of the halting problem.
Give the basic idea of the proof that the halting function isn’t computable.

Why this is important:

This is the beginning of learning formal computability. This allows us to think about computation and it's intrinsic limitations. The first step to reasoning about Artificial General Intelligence will be understanding how it can be done before we worry about its practical feasibility.
The halting problem is a pervasive and annoying problem. It’ll come up again and again, in many disguises. If we could solve the halting problem, things would be easy. Since we can’t, things are hard. Understanding the limitations it imposes is important.

For every lesson you have 2 options: do the whole thing, or skip to the questions and exercises in the end. The latter option is for people who suspect they already know the subject. It serves as a means of verifying or falsifying that hypothesis.