The Github user doesn't even exist.

Who writes Lean code in the actual paper but doesn't create a repo or even a username?