Pure Type Systems Formalized

In doing this work of formalizing a well known body of mathematics, we spent a large amount of time solving mathematical problems, e.g. the Thinning Lemma. Another big problem was maintaining and organizing the formal knowledge, e.g. allowing two people to extend different parts of the data base at the same time, and finding the right lemma in the mass of checked material. We feel that better understanding of mathematical issues of formalization (e.g. names/namefree, intentional/extentional), and organization of formal development are the most useful areas to work on now for the long-term goal of formal mathematics.

Finally, it is not so easy to understand the relationship between some informal mathematics and a claimed formalization of it. Are you satisfied with our definition of reduction? It might be more satisfying if we also defined de Bruijn terms and their reduction, and proved a correspondence between the two representations, but this only changes the degree of the problem, not its nature. What about the choice between the typing rules Lda and Lda'? There may be no “right” answer, as we may have different ideas in mind informally. There is no such thing as certain truth, and formalization does not change this state of affairs.