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 .