Automath was the hiostorically first logical framework. The goal of the Automath project was to provide a tool for the formalization of mathematics without foundational prejudice.