The last mile: How do we make AI theorem provers which work in the real world for real users and not just on benchmarks?

Abstract: As AI research progresses, we are seeing massive gains on formal math benchmarks like MiniF2F and challenges like the IMO. However, these gains are not directly accessible to the typical ITP user, nor are they used to build formal mathematical libraries. Is this because the technology is not as good as promised or because there is a disconnect between research and the day-to-day needs of users? I propose that even today, we have sufficient AI technology to enhance the experience of proof assistant users significantly. I approach this from the lens of product-focused software engineering. How do we bridge “the last mile” to make a useful product for the end user?

machine learninglogic in computer sciencemathematical softwareMathematics

Audience: learners

( slides | video )

Lean Together 2025

Series comments: Most of the talks from the conference are available on YouTube: www.youtube.com/watch?v=ZPPDktjL1Lw&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg