Last semester, I took the Senior Seminar class at UML, which all math majors are required to take. In that class, you work with a professor and write an expository paper on a certain topic of your choice. I did mine on the Curry-Howard correspondence.

Maybe you’ve heard of theorem provers before, like Lean or Rocq, formerly Coq. They’re really just programming languages with extremely powerful type systems, powerful enough that you can encode arbitrary logical propositions and even predicates as types. Creating a value of such a type is how you prove it to be true. The principle that allows this to work is the Curry-Howard correspondence, which says that types in a programming language correspond to logical formulas.

I could go on and spill more ink explaining it here, but I think you’ll probably be better served watching the presentation I gave at the end of the semester about it. The audience was the UML math department faculty, so it was definitely aimed at mathematicians, but I think it should be pretty accessible to anyone who knows a little about programming and logic. My younger sister, a sophomore also at UML, attended the talk and she said she understood a good amount of it.

From the presentation, you’ll learn about some other interesting things related to Curry-Howard like the Tarski high school axioms and get a very quick intro to category theory towards the end. Even though this talk contains so much interesting knowledge, it pales in comparison to the amount contained in the paper I wrote which was the actual goal of the Senior Seminar class. It’s almost 50 pages long and covers a lot of stuff not in the presentation, like existential types, extensions to classical logic, and even proving an actual mathematical theorem. I hope you enjoy it.