Native install instructions don't work

[jgarvin]

Evaluating:

(use-package lean4-mode
  :commands lean4-mode
  :vc (:url "https://github.com/leanprover-community/lean4-mode.git"
            :rev :last-release
            ;; Or, if you prefer the bleeding edge version of Lean4-Mode:
            ;; :rev :newest
            ))

Results in this message at startup:

Required package ‘lsp-mode-8.0.0’ is unavailable

My understanding is that melpa uses timestamps for version numbers, but the README is saying to get dependencies from MELPA, so the expectation for 8.0.0 seems wrong? But I'm not an emacs packaging expert.

This is with emacs 30.2 on Linux.