AI Will Become Mathematicians' 'Co-Pilot'

• lean4

  56 4,460 10.0 Lean

  Lean 4 programming language and theorem prover

  

• InfluxDB

  www.influxdata.com featured

  Purpose built for real-time analytics at any scale. InfluxDB Platform is powered by columnar analytics, optimized for cost-efficient storage, and built with open data standards.

  

• approxmc

  1 70 8.5 C++

  Approximate Model Counter

  

  Proofs and proof checking is also big in SAT solving (think: MiniSat) and SMT (think: z3, cvc5). It's also coming to model counting (counting the number of solutions). In fact, we did one in Isabelle for an approximate model counter [1], that provides probabilistically approximate count (a so-called PAC guarantee), which is a lot harder to do, due to the probabilistic nature.

  [1] https://github.com/meelgroup/approxmc

• lets-prove-leftpad

  5 641 6.6 SystemVerilog

  Proving leftpad correct two-dozen different ways

  [shameless plug]I maintain a collection of proofs of leftpad in different prover languages, so people can compare them. It's here: https://github.com/hwayne/lets-prove-leftpad

  [/invalid closing tag]

• holnat

  1 1 1.6 OCaml

  HOL Light Native

  I would recommend HOL Light and Lean. HOL Light is no longer being developed. It's very self contained and the foundation is very simple to comprehend. It's great for learning ATP, not the least due to the fact that Harrison wrote a nice companion book. And OCaml these days is very easy to access. I also developed a way to run it natively (https://github.com/htzh/holnat), which, while slightly less pretty, makes loading and reloading significantly faster.

• hol-light

  2 408 7.7 OCaml

  The HOL Light theorem prover

  Thanks.

  There's also https://github.com/jrh13/hol-light which I think is still maintained (just learned about it in https://www.youtube.com/watch?v=uvMjgKcZDec from this thread: https://news.ycombinator.com/item?id=40619482)

• SaaSHub

  www.saashub.com featured

  SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

  

Suggest a related project