Automated Reasoning Group

## Haiku

This page is devoted to haiku on the subject of theorem proving. For those who don't know, a haiku is a poem that is 17 syllables long. (Beginners, like us, may want to break this down into 3 lines: the first having 5 syllables, the second 7, and the last 5.) Here are some efforts:

 ``` Theorem proving sucks I don't know why we bother What a waste of time. ``` ``` - Michael Norrish ``` ``` The sun spills darkness A dog howls after midnight Goals remain unsolved. ``` ``` - Chris Owens ``` ``` Forgotten lemma? Shameless optimist! Use HOL, then you know it's right. ``` ``` - Mark Staples ``` ``` crazy semantics embedded in a prover raises exception ``` ``` - Daryl Stewart ``` ``` No more goals remain Out the door, down the dark road Unknowing city. ``` ``` - Konrad Slind ``` ``` It's blatantly clear You stupid machine, that what I tell you is true ``` ``` - Michael Norrish ``` ``` I know not a thing to do with theorem proving - somehow, life goes on. ``` ``` - Kona Macphee ``` ``` Cherry blossoms fade Their beauty is gossamer Theorems are blossoms ``` ``` - Phil Windley ``` ``` HOL words frighten me; Axiomatization, In particular. ``` ``` - Robert Beers ``` ``` Theorem proving and sanity; Oh, my! What a delicate balance ``` ``` - Victor Carreno ``` ``` This chip is correct? Well no, but it's verified Which means what? (you know) ``` ``` - Evan Cohn ``` ``` What is, may be seen Suck and see, the answer is, But may not be, known ``` ``` - Gerard M Blair ``` ``` In the cool morning A man simplifies, a goal A theorem is born ``` ``` - Don Syme ``` ``` Axiom of choice Hilbert's epsilon serene I construct no more ``` ``` - Don Syme ``` ``` Co-inductive set I do not transgress your rules You are well-founded ``` ``` - Don Syme ``` ``` Formalization: dense phrasing... obfuscation is side benefit. ``` ``` - Trent Larson ``` ``` In finding the truth Found a tool to demonstrate false and so what now ? ``` ``` - Dirk Van Heule ``` ``` Isabelle doesn't understand me. I don't speak her meta-language. ``` ``` - Claire Quigley ``` ``` Original goal. Multiple nested lemmas; tangled tree of truth. ``` ``` - Peter Homeier ``` ``` Discouraged by haiku, I decide to avoid it: Isabelle's too hard. ``` ``` - Keith Wansbrough ``` ``` Hah! A proof of False. Your axioms are bogus. Go back to square one. ``` ``` - Larry Paulson ``` ``` Fools seek certain truth. That precious pearl is hidden! Nothing can be proved. ``` ``` - Larry Paulson ``` ``` another failed proof frustration grows as a tree blame it on hardware ``` ``` - Isua Eliazar ``` ``` I'm no good at this. I proved everything is false. Surely some mistake? ``` ``` - Silas S Brown ``` ``` Meson search level........ Meson search level........I think Its time for coffee. ``` ``` - Hugh Anderson ``` ``` Don't seek refuge here. Your proof attempts are hopeless. Use Otter instead. ``` ``` - Bill McCune ```

Long-term projects