Automath («автоматизация математики») — это формальный язык , разработанный Николаасом Говертом де Брейном , начиная с 1967 года, для выражения полных математических теорий таким образом, чтобы включенная автоматическая проверка доказательств могла проверить их правильность.
Система Automath включала в себя множество новых понятий, которые позже были приняты и/или заново изобретены в таких областях, как типизированное лямбда-исчисление и явная замена . Зависимые типы — один из выдающихся примеров. Automath также была первой практической системой, которая использовала соответствие Карри-Ховарда . Предложения были представлены в виде наборов (называемых «категориями») их доказательств, и вопрос о доказуемости стал вопросом о непустоте (населенность типов ); де Брюйн не знал о работе Ховарда и независимо изложил переписку. [1]
LS van Benthem Jutting, в рамках этой докторской диссертации. в 1976 году защитил диссертацию, перевел « Основы анализа» Эдмунда Ландау на язык автоматизма и проверил ее правильность.
Однако в то время автоматика никогда не получила широкой огласки и поэтому не получила широкого распространения; тем не менее, он оказал большое влияние на более позднюю разработку логических структур и помощников по доказательству . [2] [3] Система Mizar , система написания и проверки формализованной математики, которая до сих пор активно используется, была создана под влиянием Automath.