skip to content

Concise - a synthesis of types, grammars, semantics

Presented by: 
Arnold Neumaier Universität Wien
Wednesday 26th July 2017 - 11:00 to 12:00
INI Seminar Room 2
(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:

The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons