William M. Farmer

Associate Professor
Department of Computing and Software
McMaster University

29 May 2002


Biographical Sketch

I received a B.A. in mathematics from the University of Notre Dame in 1978. I attended graduate school at the University of Wisconsin-Madison, receiving an M.A. in mathematics in 1980, an M.S. in computer sciences in 1983, and a Ph.D. in mathematics in 1984. From 1985 to 1997, I was a research scientist at The MITRE Corporation where I conducted research in computer theorem proving, formal methods of computing, and information security. After leaving MITRE, I taught at St. Cloud State University from 1997 to 1999, and joined McMaster University in 1999.

Research Interests

My primary research interests are now applied logic, mechanized mathematics, and rigorous methods of software development. I am especially interested in the logical foundations of mechanized mathematics and the little theories method for organizing mathematical knowledge. From 1990 to 1993, I was the principal investigator of a MITRE-Sponsored Research project to develop the IMPS Interactive Mathematical Proof System. The project produced a new logic and methodology for formalizing mathematics as well as the design and implementation of the IMPS system consisting of over 70,000 lines of Lisp code. I am currently leading a project called MathScheme. Its objective is to integrate and generalize computer theorem proving and computer algebra. MathScheme has received "seed" funding from Bell Canada and MITACS, a Canadian Network of Centres of Excellence (NCE) devoted to the Mathematics of Information Technology and Complex Systems.

Position Statement

Mathematical knowledge is vital to all science and engineering. However, the body of mathematical knowledge -- which is immense and growing bigger every day -- is largely inaccessible to scientists and engineers. Most new mathematics has never been written down; the highlights are presented in mathematical journals, but the details reside only in the minds of mathematicians. Computer algebra systems embody tremendous amounts of mathematical knowledge, but they reveal only the answers to queries, not how the answers were computed or why they are known to be correct. Computer theorem proving systems contain powerful deductive reasoning mechanisms and carefully organized libraries of mathematical knowledge, yet exceedingly few mathematics practitioners possess the background and dedication needed to use them. Relatively little mathematics is presented on the Web; there is no worldwide digital library of mathematics.

Sophisticated, computer-supported organization and management is needed to make mathematical knowledge widely accessible. Mathematical knowledge must be stored in general forms from which specific mathematical facts can be generated on the fly as needed. The background context of the assumptions and definitions in force must be fully captured and open to the user. The user must have the freedom to ignore or examine the details of how an answer was computed or why a statement is true. The great interconnectedness of mathematics must be represented in a way that enables the user to freely switch from one perspective to another. And the user needs to be able to read and write mathematics using his or her own notation and conventions.

Mathematics is a process of creating mathematical models, exploring them using deduction, computation, and visualization, and connecting them when they share structure. Mathematical knowledge is a byproduct of the process. Managing the mathematics process is key to managing mathematical knowledge. Scientists, engineers, and mathematicians need knowledge about existing models, but they also need knowledge about the new models they create. In most cases, new models are created by modifying or extending existing models. If the process that was used to produce and study these existing models was well managed, knowledge about the new models can be efficiently discovered and, in some cases, even automatically generated. Mathematical knowledge divorced from the process that produced it is like a theorem whose proof is forgotten.

Publications