\documentclass{letter}
\usepackage{mathpazo}
\usepackage{url}
\usepackage{hyperref}
\usepackage{breakurl}

\usepackage[official]{eurosym}
%\usepackage[scaled=.84]{beramono}

\newcommand\tlaplus{TLA\smash{\kern-.1ex\textsuperscript{+}}}
\newcommand\tlaps{\tlaplus{} Proof System}

\newcommand\httpx[2]{\href{http:#1}{#2}}
\newcommand\http[1]{\httpx{#1}{\nolinkurl{#1}}}
\newcommand\email[1]{\href{mailto:#1}{\nolinkurl{#1}}}
\newcommand\const[1]{\textsf{#1}}
\newcommand\keyw[1]{\textbf{#1}}

\newcommand\cpp{C\raise.1ex\hbox{+}\raise.1ex\hbox{+}}

\hyphenation{data-type data-types co-data-type co-data-types Isa-belle}

\begin{document}

\thispagestyle{empty}

\centerline{\large \bfseries Complex Analysis and Cauchy's Integral Theorem in Lean}

\medskip
%\vskip1.5\smallskipamount

\begin{description}
\item[Topic:] Logic, Verification, Mathematics
\item[Location:] Vrije Universiteit Amsterdam, The Netherlands
\item[Supervisors:] ~\\[\jot]
  Dr.\ Gabriel Ebner (\email{g.e.ebner@vu.nl}) \\
  Dr.\ Robert Y. Lewis (\email{r.y.lewis@vu.nl}) \\
  Dr.\ Jasmin Christian Blanchette (\email{j.c.blanchette@vu.nl})

%\item[Senior Researchers:] ~\\
%Dr.\ Stephan Merz (\email{stephan.merz@loria.fr}, Inria) \\
%Dr.\ Christoph Weidenbach (\email{weidenbach@mpi-inf.mpg.de}, MPI)
\item[Background:] ~\\[\jot]
\textbf{Proof assistants} (also called interactive theorem provers) make it
possible to develop computer-checked, formal proofs of theorems. The primary
advantage of formal proofs is the extremely high trustworthiness of the result.
%
Proof assistants are employed for hardware and software verification at AMD and
Intel. Two recent groundbreaking applications are a verified C compiler and a
verified operating system microkernel. They are also increasingly being used
by mathematicians to check mathematical proofs.

\vskip1.5\smallskipamount

\textbf{Lean} [1] is a disruptive proof assistant developed at Microsoft
Research and Carnegie Mellon University.
Lean draws on decades of experience in interactive and automatic theorem
provers (e.g., Coq, Isabelle/HOL, and Z3).
It is
based on type theory, a highly expressive logic with a very rich dependent type system
(similar to Coq's) that can capture correctness properties of programs (e.g., ``the \texttt{quicksort}
function returns a sorted list''). It is implemented in \cpp{}.

%is a new system based
%on similar ideas but takes a fresh look at many of Coq's design decisions. It
%puts the emphasis on efficiency, trustworthiness, and automatic proof
%generation, and has the potential to become a serious competitor to Coq.
%It is implemented in \cpp{}.

\vskip1.5\smallskipamount

\item[Objective:] ~\\[\jot]

To formalize modern mathematics, we must build libraries and theories about older mathematics. There is more to this than simply defining objects and writing theorems. A well-designed library has complete APIs for structures, good documentation, and tools for updating and maintaining code.

\vskip1.5\smallskipamount

Different libraries of formal mathematics focus on different topics. The standard library for Lean, \texttt{mathlib} [2], has significant developments in algebra and topology but has little analysis. Lean Forward [3], a project at the Vrije Universiteit Amsterdam, aims to formalize modern results in number theory. But these results depend on background results from many other areas.

\vskip1.5\smallskipamount

There are two main goals of this internship project.
\textbf{The first goal is to develop formal libraries of complex analysis in Lean.}
A target result would be Cauchy's integral theorem, or generalizations like [4].
This theorem is a major component needed for proving results about modular forms,
which are a focus of Lean Forward and important for modern number theory.
\textbf{The second goal of this project is
to improve how the mathematical content of the library is displayed to and accessed by internal users.}
Lean has a powerful \emph{metaprogramming} framework [5]
for inspecting its own definitions.
This framework has been used [6] to implement tools for generating documentation [7].
The library contains a huge amount of mathematical information in many different formats,
and we are interested in ways of collecting, processing, and presenting this data.


\vskip1.5\smallskipamount

This internship is an ideal opportunity to familiarize oneself with proof
assistants and to get acquainted with the exciting research taking place at
the \textbf{Vrije Universiteit Amsterdam}.
This work will likely be part of a publication at an international
conference (e.g., \emph{Certified Programs and Proofs} or \emph{Interactive
Theorem Proving}).

\item[Requirements:] ~\\[\jot]
We expect the student to be familiar with the $\lambda$-calculus and both
imperative (e.g., Python or \cpp) and functional programming (e.g., Haskell or OCaml)
and to have a basic understanding of logic. We do \emph{not} expect
familiarity with a proof assistant, although students who have used Coq will find Lean familiar.
Knowledge of Dutch is not required.
Depending on the state of the world next year,
the internship could be on-site or remote.

\item[Compensation:] ~\\[\jot]
In addition to any compensation offered by the intern's home institution, we offer \euro{250} per month and will reimburse travel expenses to Amsterdam.

\item[References:] % ~\\[0pt]
\end{description}

\kern-3.5\smallskipamount

\begin{raggedright}
\begin{itemize}


\item[{[1]}] Leonardo de Moura,
               Soonho Kong,
               Jeremy Avigad,
               Floris van Doorn, and
               Jakob von Raumer. \emph{The Lean Theorem Prover (System Description).}
  CADE 2015, pp.~378--388.


\item[{[2]}] The mathlib Community. \emph{The Lean mathematical library.}
https://leanprover-community.github.io/papers/mathlib-paper.pdf

\item[{[3]}] \url{https://lean-forward.github.io}

\item[{[4]}] Wenda Li and Lawrence C.\ Paulson. \emph{A Formal Proof of Cauchy's Residue Theorem.} ITP 2016.

\item[{[5]}] Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura. \emph{A Metaprogramming Framework for Formal Verification.} ICFP 2017, pp.~1--29.

\item[{[6]}] Floris van Doorn, Gabriel Ebner, and Robert Y. Lewis. \emph{Maintaining a Library of Formal Mathematics.} CICM 2020.

\item[{[7]}] \url{https://leanprover-community.github.io/mathlib_docs/}

\end{itemize}
\end{raggedright}

\end{document}
