[FOM] Talk on Formal Verification

[Timothy Y. Chow]

I wrote:

> Even if you don't think this will happen, the point is that this sort of 
> thing could happen, and we are already witnessing baby examples of it 
> like the proof that checkers is a draw.

Here's one more remark.  If it helps to give a couple examples of more 
mainstream mathematical theorems that involve nontrivial semiformal 
computations, consider the 290 theorem---

http://math.stanford.edu/~vakil/files/290-Theorem-preprint.pdf

---or the q-TSPP theorem---

http://www.koutschan.de/data/qtspp/

Tim