Recent posts on formal proofs usually talk about Lean, Rocq, Isabelle and (due to this post) Metamath.
What do people think of F* [1]? At least, for non-mathematics projects, doesn't it seem to be a more appropriate option [2]? It seems even the CS community is gravitating towards Lean.