Proof Technology and Ideas
José Manuel Rodríguez Caballero
josephcmac at gmail.com
Fri Mar 5 02:05:37 EST 2021
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>
More information about the FOM
mailing list