Math ∩ Computer Science: the relationship between programs and proofs
Stavan Jain (Duke University)
- While ChatGPT and other generative language models have been shown to be useful in explaining concepts and ideas in mathematics, their performance is exceedingly underwhelming when it comes to proving theorems. These forms of Artificial Intelligence have no notion of truth and instead produce output based off probability distributions computed from imperfect data. However, computer systems grounded in logical consistency through a novel interpretation of programs and proofs have recently indicated that they have the potential to transform the way that mathematicians and computer scientists prove theorems.
This talk will unravel the relationship between computer programs and mathematical proofs. The first half will build up the mathematical machinery and historical context to explain the conceptual bridge that connects programs and proofs [the Curry-Howard Isomorphism]. The second part will explore the potential implications of (computer) proof assistants on the mathematical community and propound the idea that students, educators, and researchers alike might benefit from this emerging paradigm.
There will be a tea before the talk (@ 4:00 PM), and pizza after (@ 5:30 PM).