use https://rocq-prover.org/ for that purpose

I used Lean for AoC last time and it’s really good.

Lean is intended by its authors to be also used as a general-purpose programming language. Lean stdlib contains an HTTP server for example.

IMO the biggest problems are the lack of documentation, instability and poor ecosystem. There are user libraries for some programming tasks (e.g. HTTP router, graphics API bindings) but they are mostly proofs of concept and not actively developed or maintained.