IMO It's cool to invoke the lean halting theorem, since the author proves the informal version of the halting theorem in the previous lesson.

See: https://tigyog.app/d/fr9uub3hqgab/r/the-halting-problem