Math-3100 Alternatives
Similar projects and alternatives to math-3100
-
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
-
-
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.
math-3100 reviews and mentions
-
The Fundamental Theorem of Algebra in ACL2
> Or there are these high level systems for proving deep theorems. Is anyone trying to fill the gap?
There's ongoing work on computable real numbers for instance the CoRN library[1], so hope is on the horizon, for instance, a recent update to the Coq Interval package adds certified plotting, that is, the library guarantees that if a function passes through a pixel, that pixel is filled[2]. There's also the user-friendly Coquelicot[3] real analysis library up to basic differential equations (e.g. Bessel function).
> It'll rearrange an equation but I can't ask it "prove this is increasing"
For a taste, here's my proof that the cube function is increasing[4]. If I wanted to create a tactic that automatically proves a function is increasing, I would use properties of increasing functions[5] to recursively break it down into trivial subcases.
[0] https://github.com/siraben/math-3100/blob/master/analysis.v
[1] https://github.com/coq-community/corn
[2] https://coq.discourse.group/t/interval-4-2-now-with-plotting...
[3] https://hal.inria.fr/hal-00860648v1/document
[4] http://ix.io/3rxD
[5] https://www.math24.net/increasing-decreasing-functions#h-pro...
Stats
The primary programming language of math-3100 is TeX.
Popular Comparisons
Sponsored