*As an aside, MIT just hired Adam Chlipala, who is another expert on using proof assistants. You might enjoy talking with him.*

I’ve already had some very enlightening conversations with him and hope to have more!

]]>For more of a “challenge,” how about the Classification of Finite Simple Groups?

No smiley needed: I’m down the hall from George Gonthier, who is working on precisely this problem. It’s actually an excellent test problem for machine-checked proof, because it’s (a) enormous, and (b) one of the pinnacles of modern mathematics. The first point means that if you can handle it, you know you aren’t missing some critical feature needed for modular proof development, and the second point means that your proof assistant can formalize all the really wild tricks that mathematicians have thought up.

As an aside, MIT just hired Adam Chlipala, who is another expert on using proof assistants. You might enjoy talking with him.

]]>