[opentheory-users] Prover9 HOL integration via OpenTheory

[Joe Hurd]

Hi Rob,

> Jacques Fleuriot and Steve Obua are on that track too, see:
> http://proofpeer.appspot.com/html/currentVersion.html#

ProofPeer is an interesting approach to the central problem of
allowing everyone to contribute to a common library. I've been toying
with the idea of using social network techniques to highlight useful
theory packages - in Hackage there are now so many Haskell packages
that it's sometimes hard to pick out the stable, popular package to
solve a particular problem.

Cheers,

Joe