Today there is considerable worldwide activity in the design, development and use of a great variety of computer systems in which the correctness of mathematical assertions can be machine checked, generally with the interactive help of the user. A major motivation for this activity has been the desire for the efficient production of correct software, together with the feeling that computers might help in the correctness checking. It is controversial whether it can be generally worthwhile and feasible to get the correctness of software to be machine checked, even with interactive human help. Clearly it will be necessary to build up libraries of machine checked mathematical theories, which can be conveniently accessed by the software developer.
In my talk I will review my own approach to the intellectual challenge to design systems and methods that can make the large scale production of machine checked formalised mathematics feasible. I will focus on the formalisation of abstract algebra in constructive type theory using the LEGO computer system.