Concise - a synthesis of types, grammars, semantics

Duration: 1 hour 6 mins

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/2526452/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	Neumaier, A Wednesday 26th July 2017 - 11:00 to 12:00


Created:	2017-08-25 15:56
Collection:	Big proof
Publisher:	Isaac Newton Institute
Copyright:	Neumaier, A
Language:	eng (English)


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 <50 man years of work) would produce a huge repository of formal statements and proof sketches ready for being formally proofchecked (possibly after completion or correction) by the formal theorem proving community. 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. Background (and, in the near future, more results) can be found on the project web page: http://www.mat.univie.ac.at/~neum/FMathL.html

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 <50 man years of work) would produce a huge repository of formal statements and proof sketches ready for being formally proofchecked (possibly after completion or correction) by the formal theorem proving community.
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.
Background (and, in the near future, more results) can be found on the project web page: http://www.mat.univie.ac.at/~neum/FMathL.html

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video	640x360	1.91 Mbits/sec	947.50 MB	View	Download
WebM	640x360	801.86 kbits/sec	387.62 MB	View	Download
iPod Video	480x270	491.94 kbits/sec	237.81 MB	View	Download
MP3	44100 Hz	250.33 kbits/sec	121.01 MB	Listen	Download
Auto *	(Allows browser to choose a format it supports)