Ok, this looks dope. The catch is that it’s tied to Lean 4.
Bookmarking it for when I do actually get started with Lean 4.
