Coq is cool partially because it can be compiled to OCaml. So you can write part of your program in Coq and prove its correctness, and then write the rest in pleasant OCaml. I believe there are some popular ocaml libraries, like bigint implementations, that do this.

Lean is designed to be a general purpose programming language that is also useful for mathematical proofs. From that perspective it’s kind of trying to be “better haskell”. (Although most of the focus is definitely on the math side and in practice it probably isn’t actually a better haskell yet for ecosystem reasons.)

If you try either, you’ll likely be playing with a programming paradigm very different than anything you’ve used before: tactic oriented programming. It’s very cool and perfect for math, although I don’t think I’d want to use it for everyday tasks.

You won’t go wrong with either, but my recommendation is to try lean by googling “the natural number game”. It’s a cool online game that teaches you lean and the basic of proofs.

By the way, don’t be scared of dependent types. They are very simple. Dependent types just mean that the type of the second element of a tuple can depend on the value of the first, and the return type of a function can depend on the value passed into it. Dependent types are commonly framed as “types that have values in them” or something, which is a misleading simplification.