Postdoc Position in Mathematics and Fundamental Computer Science

The postdoc position focuses on creating a new generation of proof assistants that combine linguistic layers with automated tools to aid in constructing certified mathematical documents. Responsibilities include designing a dependent type system, implementing mathematical semantics, and utilizing machine learning for formalization of type theory theorems.