The Fundamental Theorem of Algebra in ACL2

• coq

  87 4,609 10.0 OCaml

  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.

  

The kernel of a proof assistant is one of the most important components because it represents the foundation of reasoning in that logical system. There's a lot of introductory literature now, such as [0][1][2][3].

> What kind of axiomatic basis is being used in ACL2 and similar systems?

ACL2 uses first-order logic and term rewriting, but this significantly hinders proof automation (done by ad-hoc searches).

> Or do the different systems have significant differences with how and what they can prove?

Yes. First-order logic can only quantify over individual elements of a set, second-order logic and quantify over sets, and so on. Higher-order logic is the foundation of assistants like Isabele/HOL light, which let you use classical reasoning.

Alternatively (and better from an engineering standpoint) are assistants based on type theory, such as Agda, Coq and Lean. Their kernels are just type checkers, which are relatively small programs, so theorem proving in those systems is literally just functional programming with a fancy type system (though exactly how those proofs are constructed is a UX choice).

> Do the systems allow explorations in reverse maths, trying to derive stuff with as little axioms as possible?

Yes, in Coq you can print out the axioms (on top of the type system) that a result depends on. See [4] for information on Coq's logic and what axioms you can safely add (they are necessary for certain areas of math).

[0] (Coq) https://softwarefoundations.cis.upenn.edu/

[1] (Agda) https://plfa.github.io/

[2] (Isabelle) http://concrete-semantics.org/

[3] (Lean) https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...

[4] https://github.com/coq/coq/wiki/The-Logic-of-Coq

• math-3100

  1 1 7.9 TeX

  Discontinued My solutions to MATH 3100 (Introduction to Real Analysis) at Vanderbilt University.

> 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...

• InfluxDB

  www.influxdata.com featured

  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.

  

• corn

  1 108 6.8 Coq

  Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

  

> 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...

Suggest a related project