Proof Technology and Ideas

[José Manuel Rodríguez Caballero]

Ignacio wrote:

> The manichean dichotomy between "technology", and mathematical
> intelectual conceptions, is illusory: there is trivial, academic,
> work, done in any field: proof assistants, FOM, information theory,
> and digital technology, are no exception...


Let's consider an example of technology: a tablet in which it is possible
to write mathematical formulas, and they are automatically transformed into
expression in a programming language and executed. Let's consider this
machine, which I will refer to as "this tablet," from the point of view of
Aristotle's four causes.

A. The material cause of this tablet is not a mathematical intellectual
conception, but the materials extracted from mines and maybe some wood
pieces.

B. The formal cause of this tablet is a mathematical intellectual
conception. In this sense, we agree.

C. The efficient cause of this tablet is the system of industries that
develop it. They are not a mathematical intellectual conception.

D. The final cause of this tablet is not a mathematical intellectual
conception but a social purpose, i.e., to help people working on
mathematics.

Now, my claim that the use of proof assistants in everyday mathematical
practice is not a fundamental problem, but a technological one, can be
reformulated in this framework as follows: all the requirements for the
material, formal, and final causes are satisfied, but there is a
requirement missing concerning the efficient cause. Indeed, for a proof
assistant for everyday mathematical practice, we have:

(i) Material cause: the same as any device related to information
technology.

(ii) formal cause: there is a well-developed theory concerning what a proof
assistant is.

(iii) final cause: most companies selling software for mathematicians would
be interested in providing such a hypothetical product to the mathematical
community. Some research communities would like to provide this
hypothetical product even as free software.

(iv) efficient cause: until now, no corporation nor research community has
integrated all the existing elements from information technology to develop
a user-friendly proof assistant. In my personal opinion, such a system
would be a combination of natural language processing like Wolfram Alpha
and the already existing technology of Isabelle/HOL.

Concerning the efficient cause, let's consider the project Alexandria:

> ALEXANDRIA will provide (1) comprehensive formal mathematical libraries;
> (2) search within libraries, and the mining of libraries for proof
> patterns; (3) automated support for the construction of large formal
> proofs; (4) sound and practical computer algebra tools.

https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/

As an everyday user of Isabelle/HOL, I am not aware of

(4) sound and practical computer algebra tools.


Indeed, this was one of my motivations for working on a compiler from the
Wolfram Language to Isabelle/HOL (work-in-progress, this is just a
prototype to show that it is possible and easy to implement, it is not a
final product):
https://www.wolframcloud.com/obj/jose.manuel.rodriguez.caballero/Published/PiCalculus.nb

I would add two more (hypothetical) points that I consider to be essential
for the interaction between a mathematician and a proof assistant (I may
work myself on a project like that after finishing my proof assistant in
the Wolfram Language):

(5) natural language programming

(6) a tactile screen interface like the tablet mentioned above.


Kind regards,
Jose M.

References:

Hankinson, R. J. 1998. *Cause and Explanation in Ancient Greek Thought*.

Falcon, Andrea, "Aristotle on Causality," The Stanford Encyclopedia of
Philosophy (Spring 2019 Edition), Edward N. Zalta (ed.), URL = <
https://plato.stanford.edu/archives/spr2019/entries/aristotle-causality/>.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210305/6e10a298/attachment-0001.html>