BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proof Assistants: From Symbolic Logic To Real Mathematics? - Larry
  Paulson (University of Cambridge)
DTSTART:20170710T133000Z
DTEND:20170710T143000Z
UID:TALK73198@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Mathematicians have always been prone to error. As proofs get 
 longer and more complicated\, the question of correctness looms ever large
 r. Meanwhile\, proof assistants &mdash\; formal tools originally developed
  in order to verify hardware and software &mdash\; are growing in sophisti
 cation and are being applied more and more to mathematics itself. When wil
 l proof assistants finally become useful to working mathematicians?<br><br
 >Mathematicians have used computers in the past\, for example in the 1976 
 proof of the four colour theorem\, and through computer algebra systems su
 ch as Mathematica. However\, many mathematicians regard such proofs as sus
 pect. Proof assistants (e.g. Coq\, HOL and Isabelle/HOL) are implementatio
 ns of symbolic logic and were originally primitive\, covering only tiny fr
 agments of mathematical knowledge. But over the decades\, they have grown 
 in capability\, and in 2005\, Gonthier used Coq to create a completely for
 mal proof of the four colour theorem. More recently\, substantial bodies o
 f mathematics have been formalised. But there are few signs of mathematici
 ans adopting this technology in their research.<br><br>Today&#39\;s proof 
 assistants offer expressive formalisms and impressive automation\, with gr
 owing libraries of mathematical knowledge. More however must be done to ma
 ke them useful to mathematicians. Formal proofs need to be legible with a 
 clear connection to the underlying mathematical ideas.&nbsp\;
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR