Creating projects in lean

Stream: Lean for the curious mathematician 2020

[Clarissa Martelli]

I keep having "leanproject : command not found" even if I keep downloading and following the steps on how to install lean and mathlib tools, how can I create a project using mac OS?

[Eric Wieser]

It sounds like your python installation isn't putting scripts on the path. Out of curiousity, does python -m mathlibtools.leanproject --help do anything?