2

Computer Algebra Systems (CAS) are philosophically interesting in that they are an aspect of the long history of treating mind as mechanism. In this respect, mathematics may be thought of as formalizing "mind" and CAS the closest approximation to a mechanical implementation. We routinely encounter formal expressions of mathematical identities (equivalence theorems) in the literature of mathematics yet there seems to be no current CAS that takes, as input, those formal expressions to extend their capabilities.

Instead, what we have, are implementations in variations of functional programming languages (LISP, Haskell, etc.) that seem, inevitably, to resort to procedural formalisms that rarely if ever appear among the vast edifice of mathematics. If anything, the identities that make up the bulk of mathematics are best thought of as relations as opposed to the degenerate (N:1) relations known as functions. One would have expected there to be, at the very least, a relational formal language (such as the predicate calculus) implemented as a domain specific language (DSL) -- specific to the domain of importing mathematical identities from the literature of mathematics.

People routinely interpret these mathematical identities in scientific and technical papers without remark on this as a remarkable capability. Yet it is also considered unremarkable that CAS are not extensible in terms of these same identities.

Why is this?

Improve this question
1
  • 1
    There are also logic programming languages such as Prolog and Janus (I wrote a compiler for Janus as part of my dissertation). These languages are based on predicates rather than functions, and have a limited form of inference. Also, database languages like SQL are based on relations, although they don't have any sort of inference. There was an extensive literature in the 70s, 80s and 90s on these kinds of languages and how they were similar to/different from mathematics.
    – David Gudeman
    Apr 12, 2022 at 18:53

2 Answers 2

Reset to default
4

What you're looking for is not a computer algebra system, but a proof assistant, such as Mizar, Coq, or Agda. Proof assistants are designed for the formalization of mathematical proofs in any field of mathematics. They are capable of "importing" theorems from any field of mathematics.

See also automated theorem provers. Automated theorem proving is very challenging in general, because computers are not (yet) able to think about mathematics in the same way that humans can. The computer simply isn't as good at proving general theorems as humans are. That's why proof assistants require the human to guide the proof. Successful automated theorem provers tend to be specialized to narrow and well-understood domains.

That brings us back to computer algebra systems. Computer algebra systems are only designed to solve certain specific problems in narrow domains, such as finding integrals or derivatives or simplifying equations. This is why they typically cannot "import" and use arbitrary theorems.

Improve this answer
2
  • To take your example of a CAS operation -- integration -- a closed form solution is clearly a theorem that can be proven given the integral form as an axiom, but it also requires various theorems of calculus that can be traced back to an appropriate foundational axioms such as ZF set theory. Moreover, CASs address an increasing range of math intersecting those of proof assistants. There is even machine learning now arxiv.org/pdf/2202.01344.pdf
    – James Bowery
    Apr 13, 2022 at 2:33
  • 1
    As an aside, it's worth mentioning that there is a new StackExchange site for proof assistants.
    – David
    Apr 13, 2022 at 4:31
-2

Yet it is also considered unremarkable that CAS are not extensible in terms of these same identities.

Why is this?

Well, presumably, because a fully "complete" system would reduce to the halting problem. No system will be able to fully capture mathematical decidability on pain of contradiction, so the question has to be about which systems of computation best capture the forms of decidable calculation of relevance to a particular field of interest.

Improve this answer
2
  • 5
    Though theorem proving is not decidable, it is semi-decidable. This means you can always just go through every possible proof, one by one, until the theorem you're trying to prove comes up, if it ever does. Automated theorem proving systems tend to do some version of this, with heuristics and strategies to find the theorems faster. The limit on the effectiveness of such systems is not self-contradiction (they do not self-contradict), but the practical problem of computation time. Such a search takes time exponential in the length of the proof (if any exists).
    – causative
    Apr 12, 2022 at 19:20
  • @causative, yes, definitely, the range of systems that can do useful proof constructions within some bound of reasonable complexity can still be quite wide and usefully and interestingly studied. I think my point is just that there is good reason in computation theory not to expect a generic "import mathematical identities" operation.
    – Paul Ross
    Apr 12, 2022 at 20:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .