BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Language and automation in mathematics - Natarajan Shankar (SRI In
 ternational)\; Leonardo de Moura (Microsoft (USA) )\; Arnold Neumaier (Uni
 versität Wien)\; Cesare Tinelli (University of Iowa)
DTSTART:20170724T100000Z
DTEND:20170724T110000Z
UID:TALK73831@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Arnold Neumaier will give a short talk on "The communication o
 f mathematics".&nbsp\; <br>This will be followed by a discussion of the in
 teraction between language and<br>automation in current proof assistants.&
 nbsp\;&nbsp\; The seminar will actually run from 11 to 12.30.<br><br>Abstr
 act for Neumaier&#39\;s talk: <br>We discuss - from a mathematician&#39\;s
  point of view - the characteristic features that make mathematics communi
 cable between people\, between people and software systems\, and between s
 oftware systems with different semantic foundations. <br> <br>This talk ha
 s a strong philosophical component\, complementing the views presented dur
 ing the Big Proofs program so far. It exposes important issues that I beli
 eve are essential for bridging the gap between the mathematics community a
 nd the formal theorem proving community. <br> <br>One of the main points m
 ade and illustrated is that the natural mathematical language is a highly 
 optimized language for the efficient communication of precise concepts and
  their relations\, whose main features are completely lost in the current 
 generation of formalizations of mathematics. <br> <br>The insights obtaine
 d are the basis of my vision for a joint future of mathematics and formal 
 verification\, and provide a background for the design choices discussed i
 n the lecture on Wednesday.<br>
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR