Abstract

(joint work with Peter Schodl, Ferenc Domes, Kevin Kofler, Andreas Pichler, and David Langer, Vienna)

This talk features the design and implementation of tools that my research group in Vienna has created to pave the way towards automatically or interactively extracting from standard mathematical literature (such as the latex source of mathematics textbooks) a formal version of all  (correct and incorrect) mathematical claims contained in it, including all claims in the proofs and all implicit information needed for their understanding. We have very encouraging performance results for certain low level partial goals in this direction.

Completing this program (which I believe to be feasible with Thus it would bridge the mathematicians' side of the current gap between mathematics and formal theorem proving.

Central to everything are the working implementation of

• (i) a very flexible type system that merges types, grammars, and semantics into an organic unity, and
• (ii) a dynamic parser for languages that change while reading a document – one of the key features present in mathematical documents.