BEGIN:VCALENDAR VERSION:2.0 PRODID:-//Talks.cam//talks.cam.ac.uk// X-WR-CALNAME:Talks.cam BEGIN:VEVENT SUMMARY:Concise - a synthesis of types\, grammars\, semantics - Arnold Neu maier (Universität Wien) DTSTART:20170726T100000Z DTEND:20170726T110000Z UID:TALK74531@talks.cam.ac.uk CONTACT:INI IT DESCRIPTION:(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 c reated to pave the way towards automatically or interactively extracting f rom standard mathematical literature (such as the latex source of mathemat ics textbooks) a formal version of all \;(correct and incorrect) math ematical claims contained in it\, including all claims in the proofs and a ll implicit information needed for their understanding. We have very encou raging performance results for certain low level partial goals in this dir ection.

Completing this program (which I believe to be feasible wit h <50 man years of work) would produce a huge repository of formal stateme nts and proof sketches ready for being formally proofchecked (possibly aft er completion or correction) by the formal theorem proving community.
T hus it would bridge the mathematicians'\; side of the current gap betwe en mathematics and formal theorem proving.

Central to everything ar e the working implementation of

(i) a very flexible type syste m that merges types\, grammars\, and semantics into an organic unity\, and
(ii) a dynamic parser for languages that change while reading a d ocument - one of the key features present in mathematical documents.

Background (and\, in the near future\, more results) can be found on the project web page: http://www.mat.univie.ac.at/~neum/FMath L.html

LOCATION:Seminar Room 2\, Newton Institute END:VEVENT END:VCALENDAR