<div dir="ltr">Dear All,<br><br>I'm currently writing my Msc thesis on the topic of natural language <-> formal proof translation, using GF, and have been highly intrigued by the dichotomy of a rule-based formalization approach as opposed to the so-called Autoformalization scheme recently outlined by Szegedy [1].<br><br>Szegedy contends "that  in  the  coming  years  we  will  see  automated systems to rival humans in general reasoning and the fastest path to achieve this is by creating automated mathematical reasoning systems via autoformalization."  <br><br>He then poses the question : "Will we ever arrive at the point where an AI agent can learn to do reasoning as well as the best humans in the world in most established domains of mathematics?"<br><br>I see interpretations of this perspective varying from extreme optimism - a new, reformulated Entscheidungsproblem whereby some "mechanical AI agent" can decide the existence of a proof better than a human, and perhaps even a priori formulate what to prove - to a highly cynical view that this is just wishful thinking from another silicon valley technocrat.  <br><br>I've heard, for instance, that Voevodsky wasn't very enthusiastic about automated proving in gereral.  Thomas Hales says of Szegedy's group : "Their ambitions are inspiring, the resources and research methodologies at Google are grandiose, but I would not personally bet on their time frame."[2]<br><br>As far as I'm aware, much of the (still) early work using machine learning in proof search targets either satisfiability problems, which is somewhat outside the interests of most type theorists[3],  or tactic-based languages like HOL and Coq [4] where the learning of a proof isn't at the level of constructing a term that could then be presented in a human legible format, and large, fairly standard libraries already exist.<br><br>My appreciation of Agda is stays true to Martin-Löf's original vision of a programming language in which one can write proofs.  I bring this up here because it seems that using machine learning to produce Agda code doesn't yet seem compatible with Szegedy's proposal - especiallty since it doesn't yet have tactics.  Other writing in [1] dicuss various other aspects of this space, yet Agda is hardly mentioned.<br><br>How do you see the upcoming role of machine learning in theorem proving, formalization, and interactive proof development, with particular reference to Agda?<br><br>Warrick<br><br><br>[1] A Promising Path Towards Autoformalization and General AI, <br><a href="https://link.springer.com/chapter/10.1007/978-3-030-53518-6_1">https://link.springer.com/chapter/10.1007/978-3-030-53518-6_1</a><br>[2] AN ARGUMENT FOR CONTROLLED NATURALLANGUAGES IN MATHEMATICS<br><a href="https://jiggerwit.files.wordpress.com/2019/06/header.pdf">https://jiggerwit.files.wordpress.com/2019/06/header.pdf</a><br>[3] Neural networks and the satisfiability problem<br><a href="https://searchworks.stanford.edu/view/13250178">https://searchworks.stanford.edu/view/13250178</a><br>[4] HOList: AnEnvironment forMachineLearning ofHigher-OrderTheoremProving<br><a href="https://arxiv.org/pdf/1904.03241.pdf">https://arxiv.org/pdf/1904.03241.pdf</a><br></div>