sop.tex

\documentclass[11pt]{article}

\usepackage[utf8]{inputenc}
\usepackage[margin=1in]{geometry}
\usepackage{microtype}
\usepackage{fancyhdr}
\usepackage{palatino}
 
\pagestyle{fancy}
\fancyhf{}
\lhead{Nathaniel T. Stemen}
\rhead{Vrije Universiteit Amsterdam}

\lfoot{Motivation Letter}

\renewcommand{\baselinestretch}{1.3}

\begin{document}

Since the use of a computer to prove the four-color theorem in 1976, computers have only gained popularity among mathematicians. While there are still reasons to dislike the original proof as lacking any insight into the problem, it stands that the computer aided in solving the question at hand. While there are many different ways a mathematician can use a computer, I see a need for developing our tools in making this interaction as seamless as possible. Email has allowed us to communicate more quickly, mathematical programming languages like Maple and Mathematica have allowed us to run previously difficult computations in seconds, online databases such as the Online Encyclopedia of Integer Sequences allow us to search for sequences across all mathematical literature, and open sources books such as the Stacks Project allow us to effectively organize and disseminate research in more meaningful ways. We can all agree computers have affected mathematics, and the better tools we have available, the more progress within mathematics we can make.

This feeling that computers are having a revolutionary affect on mathematics has driven me towards two main fields; automated theorem proving, and formal verification. It has also taken me down side streets towards areas like homotopy type theory, constructive mathematics, and category theory where we see ideas from formal verification at play. I first learned about formal verification after learning about the Coq proof assistant where I then read about the other languages available such as LEAN, Isabelle and Agda. Once I understood some of the basic ideas of formal verification I began to think about how we can harness this power of formal verification to automate certain extensions/generalizations of theorems, lemmas, etc. Vrije Universiteit Amsterdam is an ideal place to pursue these studies because of the two main projects being undertaken by the theoretical computer science department; the Matryoshka Project, and Lean Forward. Both of these projects are pushing forward computers ability to automates pieces of mathematics and I think that's fascinating. With a plethora of researchers working in this field, I believe VU Amsterdam will be a great place to get exposed to a variety of ideas within the field of formal verification and ATP.

With my experience in both software development, and mathematical research, I think my chosen field is an ideal fit. My software development experience has taught me how to organize and build large codebases with thorough test coverage, maintain libraries, and manage product releases. On the other hand my experience in research has taught me how to dissect problems, develop my mathematical maturity, and use available tools to solve the question at hand. Over the past two years I've been able to explore my mathematical interests by attending mathematics conferences, and have attended talks ranging from modeling pedestrian dynamics, to category theory. This process has landed me on the fields of ATP and formal verification because of the belief that computers will play an increasingly important role in mathematics through the coming decades. With the proper tools, and careful foresight, the mathematician-computer interface can be made seamless and extremely beneficial. With a program that made for this very subject, I believe VU Amsterdam to be one of the best places to study this field.

\end{document}