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?
Are you thinking of ACL2?
- Daniel
P.S. Who was working on the hardware for financial transactions?