Polish scientist Andrzej Trybulec founded the Mizar project (for computer checking of mathematical proofs). When he wanted to fly to Canada, he had troubles: the only airline that would allow him to smoke was run by a Muslim country and would not let him drink. Solution: drink BEFORE the flight. I asked him how many lines of proof he could formalize in Mizar per hour. His reply: "Drunk or sober?"

Previous Home Next