Our great sponsors
-
Interesting, if you're not familiar with this space, most theorem provers like lean [1]], coq [2] and isabelle [2] are concerned with formalization, and interactive theorem proving.
I initially thought "why do we need another one of these". There's another large-scale research project already underway at Cambridge [3].
I thought this extract from Gower's longer manifesto captured the heart of the problem they're trying to solve:
>"(just consider statements of the form “this Turing machine halts”), and therefore that it cannot be solved by any algorithm. And yet human mathematicians have considerable success with solving pretty complicated looking instances of this problem. How can this be?"
Essentially, they're trying to understand what kind of algorithms can prune the search space to generate proofs, using a "Good Old Fashioned AI" Approach, rather than machine learning.
-
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.
