[Alta-Logic] CPSC Invited Speaker - Jeremy Avigad - Wednesday March 14th, 2018 at 14:00 in ICT 616

[Richard Zach]

cid:image001.gif at 01D2D60B.470FAE40cid:image002.gif at 01D2D60B.470FAE40

Computer Science Invited Speaker

*“Formal Methods in Mathematics and the Lean Theorem Prover”*

*presented by*

**

*Jeremy Avigad*

**

*Hosted by*

*Robin Cockett*

*//*

*Date:*                Wednesday March 14th, 2018

*Time:*               14:00

*Location: *ICT 616

*ABSTRACT:*

In computer science, the phrase "formal methods" is used to describe a 
body of logic-based methods that are used to specify, develop, and 
reason about hardware and software systems. These methods can equally 
well be used to discover and verify mathematical claims, however, and 
the boundary between mathematical and computational applications is not 
a sharp one. In this talk, I will survey some of the ways that formal 
methods have begun to make inroads in ordinary mathematics, and some of 
the theoretical and practical challenges that arise.

I will also discuss a new open-source theorem prover, Lean, which is 
designed to support mathematical reasoning as well as hardware and 
software verification. I will describe Lean's logical foundations and 
some of the design decisions that were adopted to meet the challenges of 
formal reasoning in mathematics.

Reference: The Lean Theorem Prover, http://leanprover.github.io/.

*BIO:*

Jeremy Avigad is Professor of Philosophy and Mathematical Sciences at 
Carnegie Mellon University. He has done work in mathematical logic, 
interactive theorem proving, philosophy of mathematics, history of 
mathematics, and automated reasoning. He is currently leading the 
library development for the Lean interactive theorem prover.

-------------- next part --------------
Skipped content of type multipart/related