ProofPeer brings together interactive
theorem proving technology with the power of the social web.
Because ProofPeer is designed to run in the cloud, exciting possibilities are opening up like easy sharing of theorem proving artifacts, machine learning applications such as collaborative filtering, and verification and computation that scale with the task at hand.
Focus on Mathematics and Engineering
We believe that interactive theorem proving can bring great benefits to (applied) mathematicians and engineers. To that end ProofPeer works hard to maintain widely accepted notation. In that way you can both profit from the hard work of your peers and also give back to the community by publishing your theorems, proofs and algorithms.
Sharing and Intelligent Versioning
ProofPeer treats your theorem proving artifacts as valuables. Once accepted by the system, they stay fresh and usable forever. Sharing of theorem proving artifacts becomes therefore painless and easy. You can continue to work with the older versions of your peer's shared theory until you are ready to switch to the new one.
Machine learning techniques help you to find and prove theorems. The more peers use ProofPeer, and the bigger ProofPeer's central database of theorem proving artifacts grows, the easier theorem proving will become for you.
Scalable Verification and Computation
Because ProofPeer runs in the cloud, its processing power is not limited by a single computer but only by the capacity the cloud can provide. ProofPeer scripts and executable algorithms that have been formalized in ProofPeer can take advantage of this raw computing power and enable you to handle your verification and computation needs in a scalable way. Nevertheless, ProofPeer also allows you to harness the computing power of your local machine.
ProofPeer currently mostly exists in our heads. To make it become reality, a lot of research and engineering still needs to be done. Therefore we keep a roadmap that keeps track of where we come from, where we are, and where we want to go.