Type inference in mathematics

TL;DR

This paper discusses type inference mechanisms in programming languages and their application in interactive theorem proving, focusing on the Mathematical Components project for verifying complex mathematical theorems.

Contribution

It explains specific type inference techniques used in the Mathematical Components project for formal verification of the Feit-Thompson theorem.

Findings

Type inference aids in automating theorem proving processes.

Mechanisms improve the efficiency of formal verification.

Application to the Feit-Thompson theorem demonstrates practical utility.

Abstract

In the theory of programming languages, type inference is the process of inferring the type of an expression automatically, often making use of information from the context in which the expression appears. Such mechanisms turn out to be extremely useful in the practice of interactive theorem proving, whereby users interact with a computational proof assistant to construct formal axiomatic derivations of mathematical theorems. This article explains some of the mechanisms for type inference used by the Mathematical Components project, which is working towards a verification of the Feit-Thompson theorem.