AI

Stream: IMO-grand-challenge

[Jason Rute]

I think the term “AI” means a lot of things to a lot of people. For one, it could just mean “write a program to solve this”. In this case that could be a imo_solver tactic written in Lean’s meta language, or a script which generates Lean code. However, it could also mean using SAT/SMT solvers and other such tools. In other ITPs, these have been built into “hammers”. Last, it could mean using machine learning—possibly neural networks and/or reinforcement learning.

[Jason Rute]

Does Lean currently have support, or is there going to be support, for hammer-like interfaces with powerful ATPs? Also, on the machine learning side, it seems that the most successful ML for ITP projects rely on having training data in the form of a dataset of proven theorems. This requires proof recording. Also, since Lean has so much syntactic sugar, it makes sense to try to strip that down to the bare bones in the training data, but to still keep the high-level tactic commands. Indeed the best AI for ITP projects, TacticToe, HOList, CoqGym/ASTactic, and ProverBot9001 all seem to rely on a good tactic-level recorded proofs stored in a simple to parse format. Moreover, to do reinforcement learning requires an interface which allows rapid back-and-forth between the proof-checker and some AI interface (attached to TensorFlow, PyTorch, etc. utilizing a GPU or many GPU machines). I think Google Research spent a lot of effort writing their own HOL Light kernel and interface to make it usable for reinforcement learning.

[Jason Rute]

I would love to see Lean with better tooling for AI, and this will better encourage users to participate. (I wrote some more rambling thoughts on AI and Lean in the AI and theorem proving stream.) I wonder if the organizers of this challenge have any plans to talk to Christian Szegedy, Josef Urban, Cezary Kaliszyk and others about how well Lean is set up for this challenge.

[Daniel Selsam]

I wonder if the organizers of this challenge have any plans to talk to Christian Szegedy, Josef Urban, Cezary Kaliszyk and others about how well Lean is set up for this challenge.

@Jason Rute Yes, definitely.

[Daniel Selsam]

I think the term “AI” means a lot of things to a lot of people. For one, it could just mean “write a program to solve this”. In this case that could be a imo_solver tactic written in Lean’s meta language, or a script which generates Lean code. However, it could also mean using SAT/SMT solvers and other such tools. In other ITPs, these have been built into “hammers”. Last, it could mean using machine learning—possibly neural networks and/or reinforcement learning.

@Jason Rute I don't think it is at all clear which if any of the existing paradigms of AI can be leveraged to win. This is one reason why I think it is a worthy grand challenge.