This talk features the design and im plementation of tools that my research group in Vi enna has created to pave the way towards automatic ally or interactively extracting from standard mat hematical literature (such as the latex source of mathematics textbooks) a formal version of all &nb sp\;(correct and incorrect) mathematical claims co ntained in it\, including all claims in the proofs and all implicit information needed for their und erstanding. We have very encouraging performance r esults for certain low level partial goals in this direction.

Completing this program (which I believe to be feasible with <50 man years of wor k) would produce a huge repository of formal state ments and proof sketches ready for being formally proofchecked (possibly after completion or correct ion) by the formal theorem proving community.

T hus 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 ve ry flexible type system that merges types\, gramma rs\, and semantics into an organic unity\, and
- (ii) a dynamic parser for languages that chan ge while reading a document - one of the key featu res present in mathematical documents.

LOCATION:Seminar Room 2\, Newton Institute CONTACT:info@newton.ac.uk END:VEVENT END:VCALENDAR