Jun 10 – 15, 2018
Tsinghua Sanya International Mathematics Forum
Asia/Shanghai timezone

Neural Program Synthesis and Neural Automated Theorem Proving, via Curry-Howard Correspondence

Jun 11, 2018, 2:00 PM
45m
Tsinghua Sanya International Mathematics Forum

Tsinghua Sanya International Mathematics Forum

Sanya, Hainan, China

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.

Presentation materials

There are no materials yet.