Seminar Details

We give an introduction to recent advances in automating mathematics through automated formalization ("autoformalization") and proof-search using deep learning, specifically transformer-based large language models. Autoformalization is the process of automatically transcribing human-written mathematical texts into computer-verifiable proofs. While most natural language mathematics looks fairly formal to the untrained eye, it can take a great deal of human effort to fully formalize mathematical text using "interactive theorem provers". Recent advances in deep-learning-based language modeling and neural-augmented proof search offer a promising path towards autoformalization and human-level mathematical AI. We present recent advances in this area as well as the challenges ahead.