Lean isn't the most loved proof assistant by mathematicians, it's not the most suited to formal verification of software, it just sort of works for both. Yet it's got the thing that's arguably the hardest to achieve, momentum. Compounded by the fact that in the AI age, the amount of publicly available human-written code directly affects how well agents can produce new code.