Ernest Davis, Department of Computer Science, New York University

In mathematics, large parts of the project initiated by Whitehead and Russell have been accomplished. Using theorem-verification technology, online libraries of mathematical proofs have been assembled which go all the way from foundational axioms to very deep theorems. Suppose that you want to do the same thing for physics; and suppose that you want the foundational point to be, not the fundamental laws of physics as we have determined them, but the experiments and observations from which the laws are derived. What would such a derivation look like? I will discuss some aspects of how such a project could reasonably be formulated, and what would be involved in it.