Speaker
Peter Koepke
(University of Bonn)
Description
From the start of AI, mathematical theorem proving has been an important challenge and technique. We sketch the topics of Automated and Interactive Theorem Proving and present the checking of naturally readable mathematical texts in the Naproche proof system. This involves translations between informal, semi-formal and formal mathematical languages and shows great potential for the use of new AI techniques.
External references
- 25040071
- e398549a-a899-4710-a05f-9de6cd76d1fd
