Proof Assistants being seriously useful for everyday garden variety serious mathematical developments

[José Manuel Rodríguez Caballero]

Harvey Friedman wrote:

> OVERALL OPINION. The prospects for Proof Assistants being seriously
> useful for everyday garden variety serious mathematical developments
> look extremely remote for the foreseeable future. However, we all know
> something about some VERY SPECIAL SITUATIONS where there is a point in
> using them. In general, I like the investment in many of these. But
> THEY ARE UNUSUAL.


I am working precisely on this problem from the point of view that is not
mainstream. My approach is to develop the proof in the Wolfram Language and
then to compile it to a mainstream proof assistant, in my case, to
Isabelle/HOL, using the Isar language of human-readable proofs. Reference
to Isabelle/Isar: https://mediatum.ub.tum.de/doc/601724/file.pdf

Ideally, the interaction between the mathematician and the proof will be
done across a WolframAlpha-like natural language programming. This work's
central premise is that what is lacking in mainstream proof assistants are
useful symbolic algebra tools and natural language programming. Here is a
theoretical reference to this last technology:
https://writings.stephenwolfram.com/2010/11/programming-with-natural-language-is-actually-going-to-work/

 Also, proofs can be visualized using the tools from graph theory provided
by Wolfram Language. One of my approach's advantages is that the
mathematician does not need to remember the name of the theorem. He/She
only needs to write the theorem, and the computer finds it. Furthermore, if
the mathematician does not remember precisely the theorem, the computer can
see it provided enough information.

Here is the Wolfram Language proof assistant (work-in-progress, the final
product will be more sophisticated, and some structures may change). I
started working on this project on February 5 of this year.
https://www.wolframcloud.com/obj/jose.manuel.rodriguez.caballero/Published/PiCalculus.nb

I think that any mathematician working on pi-calculus can correctly
understand the proofs that I formalized (it is almost as paper). It is
interesting to compare my proofs with the proofs submitted to archived
formal proofs by Jesper Bengtson (library:
https://www.isa-afp.org/entries/Pi_Calculus.html, slides:
http://www.csc.kth.se/tcs/phdseminars/slides/bengtson060529.pdf)

The main theoretical difference is that Jesper Bengtson's approach is based
on the formalization of nomial logic in Isabelle/HOL. In contrast, my
approach is based on the primitives of the Wolfram Language. Furthermore,
despite the differences of these formal systems (Jesper Bengtson's is based
on labelled semantics whereas my pi-calculus is based on reduction
semantics), a compilation is possible.

One immediate application of pi-calculus is to formalize knot theory in the
Wolfram Language. This can be done using the correspondence between
processes and knots due to L.G. Meredith, David F. Snyder:
https://arxiv.org/abs/1009.2107

Knot theory was also formalized in Isabelle/HOL, but the formalization is
not based on pi-calculus. The author following the approach from L. H.
Kauffman's book "On Knots".  library:
https://www.isa-afp.org/entries/Knot_Theory.html, paper:
https://link.springer.com/chapter/10.1007/978-3-319-22102-1_29, book
inspiring the formalization: https://zbmath.org/0627.57002

<https://writings.stephenwolfram.com/2010/11/programming-with-natural-language-is-actually-going-to-work/>
Kind regards,
José M.

--


José Manuel Rodriguez Caballero


arvutiteaduse instituut / Institute of Computer Science

Tartu Ülikool / University of Tartu


Homepage:
https://www.wolframphysics.org/people/jose-manuel-rodriguez-caballero/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210224/4b5c1e74/attachment.html>