[lacker]

It's a much newer project than Lean, and Lean has more adoption. But the vast majority of mathematicians aren't using formal methods at all, so perhaps the space is still oepn.