Another one bites the dust

Way back in 1990 I started a Phd at Cambridge University Computer Laboratory in the area of automated theorem proving. My interest at the time was around the synthesis of functional programs from mathematical proofs of their correctness, but I remember that one of the groups at the computer laboratory was interested in implementing the real numbers in one of the programming logics that they used (HOL). Since those days, things have moved on a lot, and in 2008 Georges Gronthier published his computer checked proof of the four colour theorem. More impressively, he and a team have recently finished a proof of the Feit-Thompson Theorem,  a complicated result from group theory.Of course, another long term computer proof attempt is the Flyspeck project, the formalisation of Thomas Hales’ proof of the Kepler conjecture which is also nearing completion.

There’s an interesting page here which records 100 mathematical theorems that have been proved in a range of theorem provers and it will be interesting to see how far the formalisation of mathematics will go in the coming years, and how many holes they find in the existing proofs in the process!

This entry was posted in Computers and Internet. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s