Hao Wang

The original aim of the writer was to take mathematics textbooks such as Landau on the number system, Hardy and Wright on number theory, Hardy on calculus, Veblen and Yound on projective geometry, the volumes by Bourbaki as outlines and to make the machine formalize all proofs (fill in the gaps). The purpose of the paper is to report work done recently on the underlying logic, a preliminary to that project.

Wang, H. "Toward Mechanical Mathematics," IBM Journal of Research and Development, pages 2-22, 1960.