What is Leo's vision for AI in Lean and the AMI?

Stream: Machine Learning for Theorem Proving

[Jason Rute]

@Leonardo de Moura I enjoyed your talk on Lean 4 at LFTCM 2022. I'm curious about one slide. You were talking about the Augmented Mathematical Intelligence (AMI) project at Microsoft (which I think is what Lean is technically under). Besides helping mathematicians and helping math education, you also have an aim to build a "Platform for Math-AI research". I want to ask if you have more vision on what that would look like?

[Jason Rute]

One thing you mentioned is building APIs which I think is great. Having followed this area for a while and having worked on such systems, I can say that getting the data and building the API is one of the more important (and thankless parts) of the task. It is further exacerbated by the fact that many such interfaces are often hacky, ad hoc, and proprietary. Theorem provers are just not designed for this task, and making an interface is usually hacked on years later. Further, many of these interfaces are unusable without the help of the original authors, or worse they are proprietary. (I believe neither OpenAI's current interface nor Meta Research's interface to Lean 3 have been released.) And the older data collection tools and API that I, Jesse, Stan wrote are likely bit rotting quickly (and, as well as in the case of my data extractor, were brittle and hacky).

[Jason Rute]

However, another challenge is that what a researcher team wants can change quickly. The paradigm in AI/ITP interaction 5 years ago is very different from today (where language models like transformers rule), and I think it will be very different in a few years again. I used to think there was a one-size-fits all interface but I don't think that anymore. I think flexibility and access to the system are most important. (Although, I would still love some coordination between separate theorem provers and AI teams so one doesn't have to keep reinventing the wheel.)

[Jason Rute]

Do you have thoughts on these challenges and what your team's vision is for addressing them?