Lean is similar to Coq. You could - state and prove things about (e.g.) C code, like the "Software Foundations" book does for Coq. However, nobody seems to be

Lean is similar to Coq. You could - state and prove things about (e.g.) C code, like the "Software Foundations" book does for Coq. However, nobody seems to be doing this with Lean and the tools are missing. - write programs in Lean4 and prove things about them. Some people are doing this a tiny little bit. - formalize pure math and publish papers about that. This is what Lean4 (and Coq) is mostly used for. The kinds of things Lean/Coq are able to practically state and prove are more general. Maybe you don't need that generality for real-world programs though.