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

[Sam Sanders]

Dear José, dear Harvey,

The following may be useful concerning this discussion:

I recall a 2013 talk by Georges Gonthier about his formalisation of the odd-order theorem.  
While this was a celebrated milestone, Gonthier also displayed a picture of the Alps, with the lowest peak
marked.  His message was essentially that the odd-order theorem was just the first step as
part of much larger project, but that the latter was infeasible at the moment.  

Currently, it seems that without fundamental new developments, formalisation efforts
are destined to “get stuck” on this kind of plateau before reaching (anywhere near) the state-of-the-art.  

I may well be wrong and welcome counterexamples.  

Best,

Sam

> On 24 Feb 2021, at 21:43, José Manuel Rodríguez Caballero <josephcmac at gmail.com> wrote:
> 
> 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
> 
> 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/
> 
>