You can read my notes on this code at https://x.st/turing-machine-halting-in-lean/

This code uses the Lean proof assistant to prove whether some simple turing machines halt or not.

Try it online

…or install Lean:

brew install elan mathlibtools
brew install visual-studio-code  # (if you don't already have VS Code)

If you're not on a Mac or don't want to use Homebrew, here's the more general Lean setup instructions.

…and then run the code:

leanproject get https://github.com/hrldcpr/lean-halting
cd lean-halting
code .