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

[Buzzard, Kevin M]

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.

Then what do you make of this https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/ (the question) and this https://github.com/leanprover-community/lean-liquid (the forthcoming answer), a progressing-at-a-rapid-rate computer formalisation of the proof of a result about which a recent Fields Medallist said "I think this may be my most important theorem to date"?

Write these systems off at your peril. It is only a matter of time before they start doing mathematics themselves. Who knows which system will start doing it first but things are happening.

Disclaimer: xenaproject.wordpress.com is my blog (but it's not my blog post and it's not my github repository, although I have contributed to it).

Kevin



________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of José Manuel Rodríguez Caballero <josephcmac at gmail.com>
Sent: 24 February 2021 20:43
To: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Proof Assistants being seriously useful for everyday garden variety serious mathematical developments


This email from josephcmac at gmail.com originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders list<https://spam.ic.ac.uk/SpamConsole/Senders.aspx> to disable email stamping for this address.



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/20210225/86492e1b/attachment-0001.html>