Email Gateway (Feb 05 2021 at 22:39): Email Gateway (Feb 05 2021 at 22:39):From: Alex Meyer <alex153@outlook.lv>
Bird's eye view is that Isabelle is __interactive__ theorem prover and in requires human intervention for the writing of theorems, definitions, proof suggestions. Leo III is trying to do the proof part automatically, without human intervention.
Artificial intelligence (neural, symbolic, hybrid neuro-symbolic) is trying to do the human part of the interaction with Isabelle. It can go from proof suggestions (neural theorem proving) through the writing of the bodies of functions (program synthesis) up to the concept generation and computational creativity for the creation of interesting mathematical concepts and theories (e.g. http://ccg.doc.gold.ac.uk/simoncolton/).
I am big fan of https://people.idsia.ch/~juergen/.
And my view (as a student) is that AI community is in the need for the universal language of the knowledge representation, the most general language possible (that can be embedded in the neural networks and that can be extracted from the results of neural network computing). And my feeling is that Isabelle is exactly such language - it can express everything, it has strong tool support, it has the richest set of content (in comparison to Coq, Mizar or Lean).
Of course the thesis "it can express everything" requires some caution (e.g. I am not sure how the termination requirement of the Isabelle code contradicts to this), but there are philosophical and empirical suggestions that very simple structures and rules (e.g. Isabelle/Pure) gan generate the complexity that is comparable to the Universe/Multiverse, see. e.g. https://www.wolframphysics.org/
We should be thankful to all those involved in building and maintaing Isabelle that we have this language, tools and culture of thoughts. There would not be possible the development of neuro-symbolic AI without the basis of the symbolic formalization efforts.
Alex
Last updated: Jul 15 2022 at 23:21 UTC