A method of writing proofs is proposed that makes it much harder to prove things that are not true. The method, based on hierarchical structuring, is simple and practical.
About the speaker:
Leslie Lamport began writing concurrent algorithms in the early '70s. He was so bad at it that he spent the next 20 years trying to figure out how to tell if his algorithms were correct. Fortunately, no-one else knew how either, so he was able to publish lots of papers, some of which were even read. He eventually realized that graduate school in math failed to teach him, or anyone else, anything useful about how to prove things. He finally figured it out, and since then has been pestering people with his ideas about proof writing.
Leslie Lamport is currently proving things at Microsoft Reasearch's Silicon Valley Campus.
Web Page: http://research.microsoft.com/users/lamport/.
Contact information:
Leslie Lamport
Microsoft Research