sung to the tune of “I don’t like mondays”, with apologies to Boomtown Rats
Created at the Marktoberdorf Summer School 2013
The silicon chip inside her head gets switched to HOL No pen and paper proofs today she’s gonna make it rigorous And now I don’t understand it, I always thought it was trivial but auto finds no proofs but there are some proofs what lemmas does she need to be shown? Tell me why – this is a theorem Tell me why – this is a theorem Tell me why – this is a theorem I’m gonna prove the first goal now An inductive fact is here assumed so I type induction x and two new goals I have to show and the simplifier solved just one The next case ain’t not obvious, but it ain’t so neat to just type sorry and auto finds no proofs but there are some proofs what lemmas does she need oh oh oh oh Tell me why – this is a theorem Tell me why – this is a theorem Tell me why – this is a theorem I’m gonna prove uh uh uh uhh the next goal now now now prove it all now And sledgehammer stopped without a metis call And nitpick says its hopeless So how could Gerwin show all the lemmas by induction and by auto Trying arbitrary, ’cause Tobias told us to better generalize but auto finds no proofs but there are some proofs what lemmas does she need to know know? oh oh oh Tell me why – this is a theorem Tell me why – this is a theorem Tell me why – this is a this is a this is a theorem Tell me why – this is a this is a this is a theorem Tell me why – this is a theorem I’m gonna prove uh uh uh uhh the last goal nowGo up
Photos