He's giving a talk, it's for the lulz

If you are giving a talk on a theorem proving programing language you're gonna want to make it fun