AIAI Seminar-24 June-Talk by Wenda Li

Speaker: Wenda Li

Title: An Overview of Autoformalisation & Formalisation of Real Closed Field in Isabelle/HOL

Abstract: In this talk, I will cover two lines of my work: using machine learning techniques to aid formalising mathematics (autoformalisation), and a formalisation project of mechanising the theory of real closed field in Isabelle/HOL. For the former, I will review the applications of autoformalisation and discuss some of the current challenges. For the latter, I will explore potential advancements in developing verified computer algebra systems within a proof assistant.