Invitations to Mathematics - Jim Fowler

Image
Jim Fowler
September 22, 2021
4:10PM - 5:40PM
Location
EA 170

Date Range
Add to Calendar 2021-09-22 16:10:00 2021-09-22 17:40:00 Invitations to Mathematics - Jim Fowler Title: Proofgramming Speaker: James (Jim) Fowler Abstract: Computers are a popular tool for numeric calculations, but computers can also do calculations with proofs.  In this introductory talk, we will use a computer as a "proof assistant" meaning that we will record definitions and theorems and, through an interactive dialogue with the computer in the language of type theory, prove some theorems. Even if you aren't interested in formalizing some piece of mathematics, the ideas are interesting and broadly accessible: type theory provides a context where propositions (which may be true or false) and proofs and sets are all mathematical objects.  For instance, a universally quantified theorem, proven constructively, becomes a function that can be applied to its inputs.  A lemma is like a subroutine.  Homotopy type theory goes farther, making an analogy between the equality of two objects and a path between those objects, so that some topological gadget like a "fibration" then has some type theoretic analogue.   EA 170 Department of Mathematics math@osu.edu America/New_York public
Description

Title: Proofgramming

Speaker: James (Jim) Fowler

Abstract: Computers are a popular tool for numeric calculations, but computers can also do calculations with proofs.  In this introductory talk, we will use a computer as a "proof assistant" meaning that we will record definitions and theorems and, through an interactive dialogue with the computer in the language of type theory, prove some theorems.

Even if you aren't interested in formalizing some piece of mathematics, the ideas are interesting and broadly accessible: type theory provides a context where propositions (which may be true or false) and proofs and sets are all mathematical objects.  For instance, a universally quantified theorem, proven constructively, becomes a function that can be applied to its inputs.  A lemma is like a subroutine.  Homotopy type theory goes farther, making an analogy between the equality of two objects and a path between those objects, so that some topological gadget like a "fibration" then has some type theoretic analogue.

 

Events Filters: