BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Isaac Newton Institute Seminar Series
SUMMARY:Concise - a synthesis of types\, grammars\, semant
ics - Arnold Neumaier (Universität Wien)
DTSTART;TZID=Europe/London:20170726T110000
DTEND;TZID=Europe/London:20170726T120000
UID:TALK74531AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/74531
DESCRIPTION:(joint work with Peter Schodl\, Ferenc Domes\, Kev
in Kofler\, Andreas Pichler\, and David Langer\, V
ienna)
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