Speaker
Greg Yang
(Microsoft Research)
Description
Curry-Howard correspondence is, roughly speaking, the observation that proving a theorem is equivalent to writing a program. Using this principle, I will present a unified survey of recent trends in the application of deep learning in program synthesis and automated theorem proving, with commentary on their applicability to the working mathematician and physicists.
