Our great sponsors
 InfluxDB  Power RealTime Data Analytics at Scale
 WorkOS  The modern API for authentication & user identity.
 Onboard AI  ChatGPT with full context of any GitHub repo.

At this point I would go with Lean because of mathlib. Mathlib's goal is to formalize modern mathematics, so many of the theorems you would need for analysis should already be there for you.


InfluxDB
Power RealTime Data Analytics at Scale. Get realtime insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in realtime with unbounded cardinality.

NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a more popular project.
Related posts
 An EasySounding Problem Yields Numbers Too Big for Our Universe
 Towards a new SymPy: part 2 – Polynomials
 It's not mathematics that you need to contribute to (2010)
 Did studying proof based math topics e.g. analysis make you a better programmer?
 [R] Large Language Models trained on code reason better, even on benchmarks that have nothing to do with code