Comparing #Lean and #Rocq (formerly known as Coq)

I thought both were theorem provers, but it seems Rocq is more for building verifiable software, while Lean is for more classical math.

So Lean might be a better fit for the math explorations #LLMs and #AI #Agents are doing for solving problems.