QED

QED is a project to build a database of formalized mathematics. One aspect of this project is the development of standards to make it possible for users of different theorem proving systems to share proofs and results. I provide the report on my talk on undefined terms at the last QED workshop and a very rough set of comments on the QED meta-logic .