lean - 从终端运行精益的自动证明检查程序

Question

在 Lean 的官方教程中，我看到了如何在 Vscode 和 Emacs 中使用 Lean 程序。我想知道如何从终端运行精益。例如，假设我编写了一个程序来检查是否存在无限多个素数，infinite_primes.lean并且我想通过执行来运行它

lean infinite_primes.lean

在终端。但是这个选项似乎不可用。