On Mon, 9 May 2005, Mike Miller wrote: > I attended Jonathan's talk. It was a good overview of how computer programs > can be used in mathematics. His interest seemed to be in pure math -- > computer proofs and such. I'm really sorry I wasn't able to make it (conflict schedules). I will point out the Coq proof assistant: http://coq.inria.fr/ Which was used to help verify the four-color theorem: http://www.ucalgary.ca/~rzach/logblog/2005/04/four-color-theorem-verified-in-coq.html I comment this because Coq is written in Ocaml. Brian