Does anyone remember a talk in which the presenter mentioned a wikipedia-style encyclopedia of mathematical proofs, in which all expressions added to the system are automatically checked for consistency? What was this project called? Thanks, Rob