ESP Biography

BEN SHERMAN, MIT grad student studying computer science

Major: Computer science

College/Employer: MIT

Year of Graduation: G

Picture of Ben Sherman

Brief Biographical Sketch:

I study formal proofs, and how we can use them for our own mischievous ends. While a formal proof does tell us that some statement is true (whatever "true" means), that's not very satisfying on its own. A proof should give us a computer program that explains why the statement is true, and lets us try to find counterexamples, only to find us always losing. In the restricted setting of geometric logic, consistent models of logical theories correspond to points of topological spaces, and this tells us how to compute with continuous objects such as real numbers or probability distributions. I'm trying to build a programming language that makes this connection effective.

Past Classes

  (Clicking a class title will bring you to the course's section of the corresponding course catalog)

C11007: Proofs and games in Splash 2016 (Nov. 19 - 20, 2016)
The four color theorem states that any map can be colored with just 4 colors such that no two regions which touch are given the same color. If you don't believe it, give me a map, any map, and I'll 4-color it for you! This is an example of how proofs correspond to winning strategies for a game: you won't be able to find a map that I can't color. This *interactive* interpretation of proof gives a concrete, testable understanding of truth. We'll explore the connection between proofs and games, and construct some proofs in the programming language Coq, which converts proofs to winning players in those corresponding games. Finally, we'll look at the game of Chomp, where it's clear the first player can always win, but it's actually quite difficult to figure out how!