-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
You should check out tools such as the Sledgehammer for Isabelle/HOL, which can often find even quite complex proofs. Lean currently has no equivalent of Sledgehammer (yet), though check out super and matryoshka.
no-one uses these in Lean. Closest thing we have to automated theorem proving that is in actual use is Lean-GPTF
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.