%  This LaTeX-file can be used to submit an application to the NWO Open Competition Domain Science M.
%  It comes without any guarantee that it works on all platforms. In case you run into problems, you can
%  contact the creator of this file by e-mail: enw-m@nwo.nl, but searching the internet might prove
%  to be a faster solution.

% Start the LaTeX-document
\documentclass[a4paper,10pt,fleqn]{application}

% Load the style sheet
\usepackage{application}

%%% More packages -JB
\usepackage{cite}
\usepackage{combelow}
\usepackage{wrapfig}
\usepackage{eurosym}
%\usepackage{hyperref}
\usepackage[T1]{fontenc}
%\usepackage{enumerate}

% Set spacing
\linespread{1.08333}


\newcommand\beforesubsub{\vspace*{-1ex}}
\newcommand\beforepara{\vspace*{-1ex}}

\renewcommand{\familydefault}{\sfdefault}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}

\newcommand\mathlibcommunity{The \texttt{mathlib} Community}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% IMPORTANT FOR BIBLIOGRAPHY %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Comment these lines when NOT using bibtex (but thebibliography)
\usepackage{natbib}
\renewcommand{\bibsection}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Set the type of application (M-1, M-2 or M-0), changes the header
\lhead{Application Form --- NWO Open Competition Domain Science---M-2, 2023--2024}

\parindent=2em

% Start the main text
\begin{document}

%  How to fill out this application form?
%
%  IMPORTANT: When writing your proposal, please take into account that it will be assessed by both expert referees as well as more broadly composed cluster committees and domain wide assessment committees.
%
% This application form consists of two parts. Part A is devoted to the scientific proposal, including abstract, summary and a justification for the project budget and also including the scientific and/or societal impact. Part B contains the name and affiliation of the main and co-applicant and additional information which is not immediately necessary for the scientific proposal but contains administrative information aiding the assessment procedure. Only Part A will be assessed by the referees and the cluster and domain wide assessment committees. Please adhere to the following rules when filling out this application form:
% * remove the examples and comments before converting the application to PDF and submitting it;
% * use the font and size as specified in the .sty-file and do not change the margins (2 cm in either direction);
% * each of the two Parts A and B should start on a new page;
% * no budget table should be included in this application form; please use the separately provided spreadsheet to construct your budget table and upload it together with this application form;
% * the basic details of the proposal (section A.1, incl. abstract and summary) are limited to one page;
% * the scientific proposal (section A.2) is limited to eight pages, which includes figures and tables, but excludes the list of literature references;
% * the motivation for and description of scientific and/or societal impact (section A.3) is limited to one page, which includes figures and tables, but excludes the list of literature references;
% * all references, including DOI’s, are listed in section A.4 literature/references;
% * it is not allowed to include hyperlinks to a personal website, to a group website or to similar information which, in fact, extends the page limit set;
%* Section A.2.4 is not intended for a (detailed) description of the applicants' CV, as the CV forms no part of the assessment. 
% * NWO signed the San Francisco Declaration on Research Assessment (DORA). DORA aims to call a halt to the irresponsible use of bibliometric indicators in assessing research and researchers. It is a global initiative for all research disciplines (for more information about this, see https://sfdora.org/). NWO implements its principles in all instruments. As a consequence, all types of quality indicators may be stated, as long as they only relate to a single key output item. Indicators that do not satisfy this guideline are excluded. For instance, this means that journal impact factors (JIF) or any other indicator that refers to a journal, publisher or publication platform may not be stated. This rule applies not only to quantitative indicators but also to qualitative descriptions of reputation. Therefore, terms such as “top journal” and “high-quality university press” may not be used either; the scientific content of a paper is much more important than publication metrics or the identity of the journal in which it was published. H-indexes and sums and averages of citations may also not be stated as these indicators do not just refer to the specific output concerned (article level), but are measured at the author level. It is allowed to mention the number of citations of a single output item that is relevant to the proposed research;
% * it is not allowed to include letters of support or documents other than required.
 
% What to submit to NWO through ISAAC?
% Upload as a separate pdf:
% * Application form;
% * Budget table;
% * If applicable: employer's statement when 
%       ~ the contract of the applicant or co-applicant (tenure track or upcoming retirement) does not cover the runtime of the project: guarantee adequate supervision of the to be appointed personnel
%       ~ the applicant is appointed on a one or two year’s probationary contract that, in case of good performance, will be turned into a permanent contract.

%%%%%%%%%%%%%%%%%%%%%%%%%%

\part{Scientific proposal}

\section{Basic details}
% Part A.1 covers some basic details of the application and contains information to aid the scientific assessment of your proposal as it contains both an abstract suited for your scientific peers and a summary for non-specialists in multidisciplinary scientific assessment committees. The individual parts have no length restriction but the total length of Part A.1 should not exceed one page.
\vspace{\baselineskip}

\subsection{Title}
%  The title should be clear and concise, and not an explanation. An acronym is optional.

\medskip

Computer-checked proofs and automation for Diophantine equations

\subsection{Abstract}
% The abstract should summarize the proposed research in a clear way and should be aimed at your scientific peers. Please bear in mind that NWO attaches the abstract to the invitation for referees. This abstract also needs to be uploaded through NWO's online application system ISAAC.

\medskip

Proof assistants have been developed for several decades, but only recently
have they started to become relevant to research mathematics.
In this project, we propose a collaboration between mathematicians and computer scientists
aiming at applying a modern proof assistant, Lean, to formally verify and develop modern research
on Diophantine equations.
These are polynomial equations whose coefficients and unknowns must be integers.
Their study is at least two thousand years old, and they play a central role in modern number theory.

Research on Diophantine equations often exhibits a rich blend of abstract proofs and concrete computations.
Both aspects can benefit from formal verification using a proof assistant.
Specifically, proof assistants can be used to formalize proofs step by step to check that they have no gaps,
and they can be used to ensure that the algorithms underlying computations always produce correct results,
something that computer algebra systems cannot guarantee.
%Obtaining very high trustworthiness in the result is not the only merit of formalization, these also include for example
At the same time, formalizing these aspects adds to the creation of a coherent library of mathematics in a rigorous logical language,
whose merits go beyond obtaining a very high level of trust in the results.

Users of proof assistants crave for more proof automation. Higher proof
automation translates into more user productivity, enabling more ambitious
formalization efforts. While the project will largely focus on formalizing
Diophantine equations, it will also serve as a case study for the development
of new proof automation, guiding the development of Lean. Our project will be
an opportunity to greatly extend the general-purpose proof automation offered
by two Lean tools, the Aesop tactic and the emerging hammer-style tool called
Lean-auto, contributing to making Lean much easier and more efficient to
use---for Diophantine equations and beyond.

\subsection{Summary}
% The summary explains your research proposal to the assessment committees which do not necessarily contain experts from your field. The members from the assessment committees are scientists having a background in the research areas covered by the NWO Domain Science.

\medskip

Proof assistants are computer programs that can be used to develop correct
mathematical proofs.
They provide an integrated development environment for
proofs and can be used to verify hardware, software, and of course
mathematics.
Proof assistants check that all proofs and computations are
correct.
This can be very useful, given the number of errors found even in
published mathematical arguments and the many issues that affect computer
algebra systems.
At the same time, this produces a digital mathematical library in a rigorous logical language,
whose merits go beyond obtaining a very high level of trust in the results.

In this project, we propose a collaboration between mathematicians and computer
scientists with the aim of employing a modern proof assistant, Lean,
to formally verify and develop modern research in number theory.
Specifically, we will apply proof assistants to the theory of Diophantine equations.
These are polynomial equations whose coefficients and unknowns must be integers.
%A famous result in the area is the resolution of Fermat's Last Theorem (i.e.,
%there are no positive integers $x, y, z, n$ such that $n \geq 3$ and $x^n + y^n = z^n$).
Famous open problems include resolving generalized Fermat equations, e.g., determining all coprime integers $x$, $y$, and $z$ satisfying $x^3+y^5=z^7$.
Diophantine equations play a central role in modern number theory,
with links to other areas such as algebraic geometry and cryptography.

For a variety of results on Diophantine equations, we will use Lean to check that the proofs have no gaps.
Since such proofs heavily rely on computations, we will also use Lean to
ensure that the algorithms that perform computations always
produce correct results, offering a much higher level of trustworthiness than
computer algebra systems.
This formalization of abstract reasoning and computations will contribute to the digital Lean mathematical library,
which can be used to systematically study the proofs themselves and generalize results in favorable cases.

In addition, the project will contribute to the development of proof
assistants. We will use it as a case study to guide the development of two new
tools that promise to make the development of computer-checked proofs more
automatic. The first tool, Aesop, automatically discovers proofs that are
relatively straightforward but possibly tedious for humans. The second tool,
the emerging Lean-auto, integrates sophisticated external proof procedures in Lean,
in the style of Sledgehammer and other hammers. Together, these tools have the
potential of making users much more productive, by automating proof steps that
otherwise would have to be carried out by users. But to achieve this, the
tools' development must be guided by real user benchmarks, for which the
versatile study of Diophantine equations seems ideally suited.

\subsection{Keywords}
% Use up to 5 keywords to describe your research proposal. NWO will use the keywords, together with the proposal, to identify suitable referees. Furthermore, keywords can aid the referees and committees to quickly understand the broad scope of your proposal.

\medskip

Computer algebra, Diophantine equations, Interactive theorem proving, Number theory, Proof automation

\newpage
\section{Scientific proposal}
% This section is limited to eight pages, including figures and tables and excluding literature references. While drafting your research proposal keep the assessment criteria from the call for proposals in mind. The two main assessment criteria are "Scientific quality of the proposal" (70%) and “Scientific and/or societal impact" (30%). For the assessment of proposals the basic principle is that the proposals must describe in a clear and concise way what will be investigated and why the proposed research should be carried out. Committee members judge your M-2 proposal in competition with M-Invest and M-1 proposals.
%\vspace{\baselineskip}

\medskip

Our project is located at the intersection of mathematics and computer
science. It will bring the fruits of computer science research in
proof assistants to an area of mathematics---Diophantine equations---that can
benefit from it. It will also improve the tools developed by computer
scientists, based on the experience of mathematics-oriented users.

\subsection{Research topic}
% This part of the proposal includes the overall aim, objectives and background. It also deals with the scientific originality and/or the innovative approach of the proposed research and investment, including its cutting-edge aspects and/or groundbreaking character.

\medskip

The overall (highly connected) aims of this proposal are to {\bf develop proof
automation in the Lean proof assistant} and to use this automation to {\bf
verify computations and theorems related to Diophantine equations}.

\beforesubsub
\subsubsection*{Background}

\medskip

Proof assistants (also called interactive theorem provers) are computer programs
that can be used to develop correct mathematical proofs. They provide an
integrated development environment for proofs and can be used to verify hardware,
software, and of course mathematics. Proof assistants check that all proofs
and computations are correct. Proofs developed using a proof assistant are
called \emph{formal proofs}, and the process of translating a pen-and-paper
proof to a formal proof is called \emph{formalization}.

For long, formalized mathematics was mostly a dream, with some notable
exceptions, including the formalization of Landau's \emph{Grundlagen der Analysis} in Automath
\cite{benthem-jutting-1977},
the formalization of the resolution to the Kepler conjecture in HOL Light and Isabelle
\cite{hales-et-al-2017},
and the formalization of the odd-order theorem in Coq
\cite{gonthier-et-al-2013}.
In the past few years, interest in proof assistants has grown among
mathematicians.
%Notable results include the formalization of the main theorem of liquid vector spaces~\cite{castelvecchi-2021-lte, LTE}.
%\footnote{https://github.com/leanprover-community/lean-liquid}.
An incomplete list of notable results follows:
%
\begin{itemize}[topsep=\jot,itemsep=-\jot]
\item the formal proof, following Ap\'ery's original approach, that $\zeta(3)$  
  is irrational in Coq \cite{mahboubi-sibut-pinote-2021};
% and Isabelle \cite{eberl-2019};
\item the formalization of the solution to the cap set problem
  in Lean \cite{dahmen-et-al-2019} (involving Dahmen);
%\item the formalization of the definition of perfectoid spaces in Lean \cite{buzzard-et-al-2020};
\item the completion of Peter Scholze's liquid real vector space mathematical
  formalization challenge in Lean \cite{castelvecchi-2021-lte,LTE};
%\item the formalization of Grothendieck's schemes in Lean~\cite{buzzard-et-al-2022} and Isabelle~\cite{bordg-et-al-2022};
\item the formal definitions of perfectoid spaces in Lean \cite{buzzard-et-al-2020}, and Grothendieck's schemes in Lean~\cite{buzzard-et-al-2022} and Isabelle~\cite{bordg-et-al-2022};
\item the formalization of the proof of the Polynomial Freiman-Ruzsa conjecture in Lean \cite{PFR}; and
 \item the emergence of a coherent Lean library of mathematics, \texttt{mathlib},
   developed by a large community \cite{mathlib-mathlib-2020}.
\end{itemize}

\looseness=-1
Despite this progress, proof assistants are not yet an integral part of the
mainstream of mathematics. This is a pity, given that flawed and
unclear mathematics abound.
%There are many disputed theorems,
%including
%Mochizuki's claimed proof of the
%\textit{a\kern0.02ex b\kern0.02ex c} conjecture \cite{castelvecchi-2015}.
%
A recent debacle is the proposed solution by Xu and Ye on classifying
three-dimensional closed vacuum static spaces:
It was published in \emph{Inventiones mathematicae},
before a flaw in a lemma (due to others) on which the classification crucially relied was discovered and the entire proof collapsed \cite{Xu-Ye-2023}.
%
More applied areas, such as cryptography, are also subject to controversies
\cite[p.\,209]{beringer-et-al-2015} \cite{pass-et-al-2017,xi-et-al-2014}.
%
Beyond the proofs themselves, there is also the question of whether computer
algebra systems such as Mathematica and SageMath can be trusted. The ``misfortunes of a trio of mathematicians
using computer algebra systems'' \cite{duran-et-al-2014} is a stark reminder
that these programs sometimes deliver wrong answers, whether accidentally or by
design.

\looseness=-1
At the same time, there are important benefits to formalization of mathematics beyond the very high
trustworthiness of the results. %, including the following.
%% @SANDER: The next sentence sounds negative somehow. Or maybe I don't get it? --JB
Finding the most appropriate representation of mathematical objects and proofs inside a formal language %of the proof assistant
often leads to structures that might be much more difficult to grasp ``by hand''.
Apart from new mathematical concepts of interest, it can also lead to new proofs.
Joint formalization efforts create an unambiguous library of definitions, theorems, and proofs, which can be queried in a robust and efficient way.
%%% REPEATS THE SAME IDEA AS BELOW
Studying proofs %---e.g., tracing where assumptions are used---
becomes available quickly and accurately, which can help in obtaining generalizations.
In proof attempts with many variables or assumptions around, formalization can assist in keeping track of these and subsequently completing the proofs.

\looseness=-1
Towards the vision of formalized mathematics, we identified an area of
mathematics that will particularly benefit from verification:\ the
research on Diophantine equations. It features a rich blend of
abstract proofs and concrete computations. Proof assistants can play an
important role with both theoretical and computational aspects.
Moreover, our project will also be useful to guide the development of proof
assistant technology, which so far has possibly been more guided by the
interests of computer scientists than of potential mathematics-oriented users.

\looseness=-1
We propose to carry out this research using the Lean 4 proof assistant
\cite{de-moura-ullrich-2021}.
Lean %is developed primarily at Microsoft Research. 
%% Leo de Moura has just moved to Amazon. --JB
has an expressive logic based on dependent type theory, and it is easy to
extend via metaprograms that rely on the same logical language that is used to
express specifications and proofs. Through its metaprogramming framework, Lean can be extended with
custom proof automation procedures.
%The Aesop proof tool
%\cite{limperg-from-2023} is an example of such automation that is making
%\texttt{mathlib} contributors much more efficient. There are also efforts
%towards developing so-called hammer-style automation
%\cite{blanchette-et-al-2016}, which delegates proof obligations to
%external automatic theorem provers, in Lean.
%
The choice of Lean 4 is also motivated by the desire to reach mathematicians.
Lean boasts a large, coherent, community-driven, open source library of
mathematics developed largely by mathematicians, called \texttt{mathlib}
\cite{mathlib-mathlib-2020}. This library, and especially the parts about
advanced number theory, will be crucial for our project.

\looseness=-1
But regardless of the
vehicle, the goal is to advance science. Despite the proof assistant
community's fragmentation, substantial advances in one proof assistant usually
translate into advances in others. Many tools have been ported, even across
systems with different logical foundations. As always, the real progress is
conceptual, not technical.

\beforesubsub
\subsubsection*{Key objectives}

\medskip

%Our overall aim is to formalize the research about Diophantine equations in the Lean proof assistant.
Our overall aims, concerning formal proof automation and its application to
Diophantine equations, will be achieved by pursuing four key scientific
objectives, which build on each other.
%
Our starting point is that there is a lot of scientific value in
combining the use with the development of theorem proving technology.
By using our own tools, we can address shortcomings as they
arise and implement new features that meet practical needs. It is also important
that the techniques and tools we develop are adopted by others and outlive the
project.
With our expertise using and developing theorem provers and our
collaborations, we are in an ideal position to achieve the stated aims.

\beforepara
\paragraph{Key objective 1: Provide white-box forward proof automation.}

%\nopagebreak

\looseness=-1
The theory of Diophantine equations is not only about computation. It is also
about logical reasoning and can greatly benefit from general-purpose automation.
%
Aesop is a proof search tactic for Lean 4 developed primarily by Jannis Limperg
under Blanchette's supervision, initially at Vrije Universiteit (VU) Amsterdam
and now at Ludwig-Maximilians-Universität (LMU) München. The tactic provides
white-box automation, meaning that users can easily extend it with custom proof
rules in a predictable way.
%
Internally, Aesop uses a tree-based search procedure that applies the
custom proof rules. % (or tactics). % In general, the rules are arbitrary tactics, and they are
%  allowed to generate new subgoals.
%When exploring the search tree,
It uses a
best-first strategy, preferring ``promising'' goals over less promising ones.
It distinguishes between safe rules, which can be applied without
backtracking, and unsafe rules. It also performs a normalization phase before
applying standard rules, notably using the standard \texttt{simp} tactic. Thus,
Aesop is useful on goals that require both some proof search and some
simplification.

\looseness=-1
Aesop has been used successfully in some case studies
\cite[Section~5]{limperg-from-2023} and was an invaluable help to the
\texttt{mathlib} developers as they ported the library from Lean 3 to Lean 4.
However, it suffers from a major limitation that reduces its usefulness. It is
much stronger at backward reasoning than at forward reasoning; yet some proof
goals would benefit from more forward steps. As an example, consider a predicate
$P$ for which lemmas of the form $\ldots \to P\; n$ abound.
%%% @JASMIN: Find concrete examples of P.
Backward reasoning
will potentially consider every such lemma, yielding an explosive search tree.
By contrast, forward reasoning would focus on deriving the conditions under
which $P\; n$ is true based on what is known to be true.

%It has no special reasoning
%capabilities for arithmetic, which is ubiquitous, and other algebraic
%procedures, including those developed as part of this project. And it cannot
%reason by induction. In addition, since it depends on user-defined proof rules,
%a lot of fine-tuning is still necessary to select the right rules for basic
%Lean theories; much of this fine-tuning is currently lacking. The objective is
%to address all these limitations.

\beforepara
\paragraph{Key objective 2: Develop hammer-style proof automation.}

  Lean already offers some general-purpose proof automation, such as
  \texttt{simp} and Aesop, but it currently lacks the strong proof
  automation provided by Sledgehammer for Isabelle (codeveloped by
  Blanchette) or HOLyHammer for HOL Light and HOL4. These \emph{hammers}
  \cite{blanchette-et-al-2016} rely on automatic theorem provers
  (e.g., cvc5 \cite{barbosa-et-al-2022-cvc5}, Vampire
  \cite{kovacs-voronkov-2013}, Zipperposition \cite{bentkamp-et-al-2021-hosup})
  to prove goals.
  Hammers typically consist
  of three main components in addition to the automatic provers
  (Figure~\ref{fig:lean-hammer-architecture}):
  the \emph{relevance filter} heuristically selects relevant definitions
    and lemmas based on the current goal; %, using either an iterative procedure or
%    machine learning;
  the \emph{problem translation} module encodes formulas from the proof
    assistant's logic to the automatic provers' usually less expressive logics%
%    The encoding should ideally be sound and complete, although good results were
%    obtained with encodings that were neither \cite{meng-paulson-2008-trans}
;
 and
  the \emph{proof reconstruction} module translates proofs generated by the
    automatic provers to proofs expressed in the proof assistant's language.

\begin{wrapfigure}{r}{0.35\textwidth}
\centerline{\includegraphics[scale=.18]{diagrams/hammer-architecture}}
\caption{Architecture of a hammer}
\label{fig:lean-hammer-architecture}
\end{wrapfigure}

  There is ample evidence that hammers can be effective. The landmark ``Judgement
  Day'' study by B\"ohme and Nipkow \cite{boehme-nipkow-2010} showed in 2010 that
  Sledgehammer could prove about half of the goals that arise in typical
  Isabelle developments. %This came as a surprise to most Isabelle
  % users
  Since then, Sledgehammer has been adopted by a large majority of users.

  A hammer called Lean-auto is being developed by the group of Jeremy
  Avigad at Carnegie Mellon University (CMU). The most advanced component is a
  tactic called \verb|duper| \cite{clune-et-al-2024}, which implements
  the $\lambda$-superposition calculus and can be used to reconstruct proofs.
  Work is going on to develop a relevance filter. Despite this
  progress, many exciting challenges related to problem translation remain open.
  The gap between Lean's logic, based on dependent type theory, and that of the
  automatic provers, based on first- or higher-order logic, is
  glaring, and naive translations result in highly cluttered, and hence
  inefficient, problems for automatic provers.

  Experience has shown that working with realistic case studies is crucial to
  make a hammer successful in practice. Indeed, most hammers have failed to
  reach users, and we do not want this fate to await Lean-auto.
  As part of this project, we will develop Lean-auto's problem encoding
  to increase its success rate, based on case studies
  related to Diophantine equations. In particular, we will ensure that type
  classes, which are ubiquitous in Lean and are also needed for Diophantine
  equations, are handled efficiently by Lean-auto.

\beforepara
\paragraph{Key objective 3: Verify Diophantine computations.}

Invoking nontrivial algorithms from number theory (and beyond) has become indispensable for solving a very wide variety of Diophantine equations~\cite{smart-1998, cohen-2007-I, cohen-2007-II}.
These range from classical, yet central, equations such as \emph{Mordell's equation} with (given) integer parameter $D\not=0$,

\begin{equation}\label{eqn Mordell}
y^2=x^3+D \quad \text{to be solved in integers $x, y$},
\end{equation}
%\pagebreak[2]
to major outstanding equations such as the  \emph{generalized Fermat equation}~\cite{Bennett-et-al-2015} with %(given) ---SD -- double-check
signature $(p,q,r) \in \Z_{\geq 3}^3$,

\begin{equation}\label{eqn GFE}
x^p+y^q=z^r \quad \text{to be solved in \emph{coprime} integers $x, y, z$}.
\end{equation}

%The use of effective methods for explicitly resolving Diophantine equations is a central and vast field with numerous different techniques.
%Mention examples (incl. own) also ``cursed curve''; see foo, or, for a more popular account, bar..
%We will focus on a range of number theoretic data, central to the resolutions of various interesting Diophantine equations as described in Key objective 4 below.
%Such number theoretic data includes 
%
% building the basics with already interesting applications
Computer algebra systems provide thousands of algorithms, but only a handful have been implemented and verified in a proof assistant.
This is a barrier to the adoption of formal methods by mathematicians who need to carry out computations.
Performing the computations step by step as logical inferences
can be extremely tedious.
%is at best very tedious and at worse virtually impossible. 

\looseness=-1
We will focus on formally verifying number-theoretic data that is key to resolving Diophantine equations such as the above.
%This roughly relates
%which roughly fall into the following two categories.
We will cover computations essential to algebraic number theory, involving rings of integers, unit groups, and class groups.
Moreover, we will build a collection of commonly used interoperable techniques to solve Diophantine equations, including methods for
basic obstructions to existence of solutions and for Diophantine approximations.

%We will mainly cover computations related to some essential algebraic number theory, involving continued fractions, rings of integers, class groups, unit groups, local obstructions, etc.
%\begin{itemize}
%\item continued fractions
%\item algebraic number theory (rings of integers, class groups, unit groups)
%\item linear forms in logarithm
%\item local obstruction (including effective lifting lemmas)
%\item $p$-adic techniques.
%\end{itemize}
% In line with key objective 1, -- no longer true --JB
For the more involved computations, we will aim at certifying external output
data inside Lean, rather than running a formally verified algorithm inside the
%trusted
kernel, which can be prohibitively slow.
In this way, we will benefit from the strong computer algebra systems already
available, which provide fast implementations of lots of algorithms.

% through speed of both evaluation and algorithm development.

  %A further advantage of
  %implementing computer-algebra-style methods in a proof assistant is that the
  %methods can be reused by future formal proof developments---about Diophantine
  %equations or other topics in number theory and beyond.

\beforepara  
\paragraph{Key objective 4: Build a formal library for Diophantine equations.}
 
%The aims for a formal Diophantine equations library are twofold, namely \emph{building a collection of commonly used interoperable techniques to solve Diophantine equations} and \emph{creating
%an explicit list of Diophantine equations with their solutions}.

\looseness=-1
We aim at creating a list of interesting Diophantine equations with their solutions.
In all cases, we aim at fully formalized proofs for every theorem statement.
%This does not mean that we will shy away from situations where the overarching Diophantine result lies beyond this formalization project, such as results depending on the modular method~\cite{Bennett-Dahmen-2013}.
%But in these situations, precise Diophantine input not relying on such techniques can be distilled and consequently formalized.
%This separation also helps make the theory more transparent.
%
%The collection of techniques serves as a bridge between the computational aspects and the (theoretical) Diophantine results obtainable from them. 
%We will aim at the following methods. Basic obstructions to the existence to solutions, 
%
%\begin{itemize}
%\item \emph{Basic obstructions to existence}.
%In its most basic form, this will entail an efficient (Hensel) lifting procedure that will certify that a given system of Diophantine equations does not have a solution modulo a (given) prime power.
%Formulations in terms of $p$-adic numbers will also be very practical, as are generalizations to number fields and their localizations.
%We are also interested in setting up flexible procedures for obstructions coming from reciprocity (quadratic and beyond).
%\item \emph{Descent.} Factorization, curves..
%\item \emph{Diophantine approximation}. From continued fractions to lower bounds for linear forms in logarithms
%\begin{itemize}
%
%Roughly speaking, we consider classical, modern, and new Diophantine results.

\looseness=-1
As a staring point, the previously mentioned classical \emph{Mordell's equation}~\eqref{eqn Mordell} can be considered, e.g., for all nonzero integers $D$ with absolute value up to some ``reasonable'' bound to vastly extend the pioneering results from~\cite{baanen-et-al-2023}. 
More generally, we can consider the \emph{superelliptic equation} with (given) integer exponent $n\geq 2$ and separable polynomial $f(x) \in \Q[x]$ of degree $d \geq 2$ (excepting $n=d=2$):

\begin{equation}\label{eqn superelliptic}
y^n=f(x) \quad \text{to be solved in integers $x, y$ (or, potentially much harder, in \emph{rational numbers} $x,y$)},
\end{equation}
\looseness=-1
for which there are many interesting instances, e.g., ternary equations.
%To aid with many of the cases above, we will resolve \emph{Thue equations}, which are also of great interest for many other reasons/applications, as are the more general 
To aid with many of the cases above, we will resolve \emph{Thue equations}, which are also of great interest for many other reasons, as well as the more general 
\emph{Thue--Mahler equations} (see, e.g., Smart \cite[Chapters VII and VIII]{smart-1998}). % cite Cohen Section 12.10?
This will bring us to central Diophantine applications such as determining all elliptic curves (say, over $\Q$) with good reduction outside a prescribed finite set of primes.

\looseness=-1
Next, we aim at formalizing recent research results.
Natural candidates include %determining perfect powers in sequences of arithmetic interest, such as
solutions to small exponent cases (where the modular method fails) of \emph{generalized superelliptic equations}.
An interesting explicit instance of this (restricting to exponents $\ell\leq5$) is the final resolution by
%%% BIG V when no first name
Van Langen~\cite{vLangen2021} (as a PhD student supervised by Dahmen) of

\begin{equation}\label{eqn fourth powers}
(x-y)^4+x^4+(x+y)^4=z^\ell \quad \text{to be solved in \emph{coprime} integers $x, y, z$}. %only x,y, comprime?
\end{equation}
Further options include perfect powers in elliptic divisibilty sequenced %, as in~
\cite{Dahmen-vLangen}.
%%% \cite{} should be parenthetical.
Finally, the generalized Fermat equation~\eqref{eqn GFE} in case $p=q \not=r$ for ``small'' primes $p$ and $r$ will be amenable to resolutions with techniques that seem within reach of formalization, at least when imposing some congruence conditions on the solutions $x,y,z$.

\looseness=-1
The latter could also include new cases.
Other new Diophantine results could be obtained as well. %in favorable cases by exploiting the power of the proof assistant. Especially it's...
Proof assistants are ideally suited for keeping track of all choices made in the solution method,
%In favorable cases, this will allow writing down 
making it natural to create very general theorems, containing, e.g., many parameters, of which the final clean results are direct specializations. 
A related, but perhaps deeper advantage is that often the strength of an underlying solution method relies on consistently optimizing choices of many dependent parameters,
at which proof assistants can provide invaluable help, e.g., by immediately pointing to all parts of a proof when small details are changed.
%e.g., in elaborate applications of linear forms in logarithms or targeted Hunter searches for number field enumaration.
%A proof assistant can immediately point to all parts of a proof when small details are changed, thereby not only making sure that complex proofs are correct,
%but also helping in optimizing parameter choices, which may lead to stronger methods and results.

Many interesting Diophantine equations could be considered.
The choice will partly depend on
library development, progress with other key objectives,
and background knowledge or preference of the hired staff.

%While list of solved Diophantine equations (with proofs of course) is of much interest in its own rights, at the same time, many types of Diophantine equations (e.g., Thue equations) serf as input to resolving other more complicates ones. Furthermore, some Diophantine equations translate into questions about other objects, involving e.g., important moduli problems.

%todo, in ideal case also?: Establishing a collection of more theoretical results concerning specific families of Diophantine equations. This would involve general finiteness statements and \ldots



\beforesubsub
\subsubsection*{Originality and innovation}

\medskip

With the growing adoption of proof assistants by research mathematicians and
the ongoing development of Lean 4, the overall aims of this project are very
timely.
The key objectives can build on each other to yield better tools and better
mathematics.
The originality and innovation aspects are present in all four key
objectives.

% Both Aesop and Lean-auto are new proof tools. They are both partly
% inspired by Isabelle tools---\texttt{auto} for Aesop and Sledgehammer for
% Lean-auto---but many aspects of their design differ from their Isabelle
% counterparts, and they face challenges particular to dependent type theory.
% Dependent type theory is a very expressive logic that features not only
% dependent types (functions $f : \sigma \to \tau$ where the type $\tau$ depends
% on the actual value of type $\sigma$ passed as argument to $f$) but also
% uninhabited types, universes, and universe polymorphism, all of which are not
% present in the simple type theory underlying Isabelle.

Specifically, our goal with Aesop is to provide strong proof automation while
supporting dependent type theory. We will build on Aesop's
strength to offer efficient forward reasoning. Some
tools, such as Isabelle's and Coq's \verb|auto|, are based
primarily on backward reasoning; others, such as Isabelle's \verb|AUTO2|
\cite{zhan-2016}, are based on forward reasoning. We believe that by combining
backward and forward reasoning under one roof, the result will be a uniquely
strong white-box automation tactic with no counterpart in any proof assistant,
increasing user productivity substantially.

%\pagebreak[2]


Our goal with Lean-auto is to obtain the first well-tuned hammer for dependent
type theory. Remarkably, CoqHammer
\cite{czajka-kaliszyk-2018} for Coq has not been widely adopted by the community,
apparently because of its low success rate in practice.
%As a case study
%\cite{czajka-et-al-2018}, the CoqHammer developers tellingly chose to port an
%Isabelle formalization instead of using of the many available Coq
%formalizations.
One explanation is that CoqHammer has poor
support for type classes. Given that they are ubiquitous in Lean, we
will make sure to support them efficiently.
%
In addition, Lean-auto will be the first tool of its kind
to integrate the new generation of efficient
higher-order provers \cite{barbosa-et-al-2019,vukmirovic-et-al-2023,
sb-21-leo3,br-20-vampire-ho-combs,bentkamp-et-al-2021-hosup}, including E
\cite{vukmirovic-et-al-2023} and Zipperposition
\cite{bentkamp-et-al-2021-hosup} developed partly by Blanchette's team.
These provers can reason efficiently about the nondependent fragment of
dependent type theory. Using suitable lightweight encodings, whose design will
be inspired by preliminary work by Cruanes and Blanchette
\cite{cruanes-blanchette-2016}, we expect Lean-auto to obtain very high success
rates, multiplying user productivity.

Other proof assistants such as Isabelle already provide some of the automation
we want to add to Lean. Indeed, some of Isabelle's automation was developed by
the co-PI. In this project, we now target a much richer logic:\ Lean's
dependent type theory. This poses many new challenges. At the same time,
dependent types are invaluable when developing a large, coherent library of
formal mathematics.

%Mathematicians are using
%Lean precisely because they determined that to develop a large, coherent
%library of formal mathematics, they need dependent types.

Invoking nontrivial algorithms from number theory (and beyond) has become indispensable in the modern resolutions of Diophantine equations.
Yet close to nothing concerning these computational aspects is available in any of the proof assistants.
There is the successful case study~\cite{baanen-et-al-2023} carried out at VU Amsterdam, but this is only the tip of the iceberg.
The proposed research will pave the way to 
bringing formal methods to the vast field of effectively resolving Diophantine equations.
This innovation also has the potential to extend to other fields. %directly as some of the algorithmic aspects also apply to these other fields, but the overall setup could act as a succesful case study

A coherent formal library for Diophantine equations (including resolution proofs) will be entirely new.
Having such formally verified results will not only
bring very high trustworthiness to the field,
but the library will also enable many other %interesting
aspects, such as structured search and study of both Diophantine results and
proofs. From the point of view of mathematicians, proof assistants constitute a
new tool that will help resolve new Diophantine equations.

%This also brings novel tools to solving new interesting Diophantine equations,
%while formalizing this at the same time.%
%\smash{\lower3ex\hbox{\llap{\color{red} todo ---SD: Clarify}}}

%Establishing suitable certificates in the context of Lean, where we have to balance classical complexity issues with representations in Lean’s dependent type system, will be part of the main research questions. As we have to efficiently cary out (possibly many times) the computation for verifying an instance of the certificate, as well as (abstractly) prove the correctness of the verification procedure for the certificate

\subsection{Approach}
% Describe which methods and techniques will be used in the proposed research and discuss their applicability and accessibility. Discuss the need, the complementarity and added value of the collaboration between the main applicant and co-applicant. Include a detailed work plan and indicate the duration of the proposed research.

\medskip

\looseness=-1
A major difficulty facing any application of proof assistants to mathematics
is that proof assistants are almost exclusively developed by computer
scientists. Much of the mathematics that has been verified so far is taught at
the undergraduate level.
% likely because this is the mathematics to which
% computer scientists have been exposed to.
%
In recent years, there has been some noteworthy developments toward the
formalization of research mathematics. Nevertheless, for many topics that
interest research mathematicians, there still exist far too few libraries and
tools. With this project, we aim to develop libraries and tools for a branch of
mathematics, Diophantine equations, that so far has received little attention
from formalizers.
A notable exception is the project of formalizing a proof of Fermat's Last
Theorem~\cite{FLT} (and earlier on the regular prime exponent
case~\cite{Best-et-al-2023}, which has now been completed), but there
the focus is on one particular famous (exponential) Diophantine equation and
its underlying methods, whereas we will consider Diophantine equations more generally.

\beforesubsub
\subsubsection*{Research methods}

\medskip

The most noteworthy methodological aspects of our project are as follows.

We will \emph{use a modern proof assistant}. Lean draws on decades of
  experience in interactive and automatic theorem provers (especially Coq
  \cite{bertot-casteran-2004} and Z3 \cite{de-moura-bjoerner-2008-z3}). The
  system's engineering is clean and efficient. A mechanism for introducing
  quotient types and a transfer tool facilitate reasoning up to isomorphism
  without resorting to setoids \cite{barthe-et-al-2003} or homotopy type theory
  \cite{awodey-2012}. We will use Lean 4, the most recent version of the tool,
  and \texttt{mathlib}.

The formal proofs and the proof automation
  will be developed with \emph{maintainability} in mind, so that they can serve as a
  basis for further research and experiments. Whenever possible, they will be
  distributed together with \texttt{mathlib}, to be available to as many users
  as possible.

In contrast to many formal proofs, which are ``write only'',
  our proofs will be \emph{readable, structured proofs}, in which
  the important steps will be clearly identified, using
  Lean's Mizar-like \relax{declarative style}. % (Figure~\ref{fig:declarative}).
  Declarative proofs
  can be used to communicate with mathematicians and are easier to port
  across systems \cite{paulson-2017-cpp}.
  As Paulson and Blanchette noted \cite{paulson-blanchette-2010}, this style is
  particularly amenable to hammers: Users specify the
  intermediate steps in a proof, invoke the hammer, and if necessary
  introduce further intermediate steps until the hammer can prove them all.
%  \begin{quote}
%  \looseness=-1
%  In Isabelle, the simple combination of structured proofs and Sledgehammer
%  takes the user surprisingly far. \dots{}
%  %In brief, [structured proofs] support
%  %natural deduction through local scopes that can introduce assumptions (using
%  %the keyword \textbf{assume}) as well as local variables and definitions.
%  %Moreover, while traditional tactic scripts contain only commands, a structured
%  %proof explicitly states the assumptions and goals.
%  When proving a proposition,
%  users can state intermediate properties that they believe to be helpful. If
%  they understand the problem well enough to propose some intermediate
%  properties, then all they have to do is state a progression of properties in
%  small enough steps for Sledgehammer to be able to prove each one.
%  \end{quote}

For the formalization parts of the project, we will aim at \emph{complete
  verification}. When proving a theorem, we will make sure that all the
  supporting lemmas are formally proved and the computational data have been
  verified. Proofs found using automatic provers integrated via Lean-auto
  will be automatically reconstructed in Lean.

We will \emph{integrate computer algebra systems} in proof assistants
  by aiming at transferring most of the more involved algorithmic tasks from the proof assistant to the computer algebra system.
  The latter then performs a computation and delivers some (possibly long) certificate that can be checked by the proof assistant.
  Among recent related work is the formal irrationality proof of $\zeta(3)$~\cite{mahboubi-sibut-pinote-2021}, involving Assia Mahboubi (who is a guest professor at VU Amsterdam),
  where Maple scripts were used to produce input for the proof assistant Coq.
  
We will build a coherent \emph{library of Diophantine techniques and results},
  mostly relying on techniques from (computational) algebraic number theory, both classical and more advanced techniques.
  We will aim at maximal generality when reasonable and more specific results when necessary, but always with usability in mind.
  The goal is that others will find it useful and build on it in the future.

\beforesubsub
\subsubsection*{Work plan}

\medskip

\looseness=-1
With support from NWO, we will hire one postdoctoral researcher and one PhD
student, both for four years.
The project will have a duration of five years.
The postdoc will be hosted by the Department of Mathematics of VU Amsterdam and is expected to have a % more
mathematics-oriented profile.
The PhD student will be hosted by the Institute for Informatics of LMU München,
and we will be looking for someone with a strong computer science background.
Ideally, both staff will feel at ease in both areas, because we are aiming at a
tight collaboration between mathematicians and computer scientists, which we
believe will result in better formalized mathematics but also better tools.

To strengthen the ties between the two teams, we will organize
frequent visits by the hired staff and the PIs. In particular, Blanchette
is still a guest researcher at VU Amsterdam %, where he supervises two PhD student,
and is expected to visit Amsterdam frequently. We will also organize two smaller
workshops and a larger one as well as an ongoing
online seminar, including collaborators such as Jannis
Limperg (Aesop's main developer, LMU München) and Alain Chavarri
Villarello (formalizer of number theory, VU Amsterdam). The two teams have
complementary skills that will be useful to the project (see also~\ref{ssec:embedding}).

The four key objectives above will be met by carrying out four tasks described
below, where Task \textit{n} corresponds to Key objective \textit{n}. Tasks
1~and~2 will be carried out by the PhD student. Tasks 3~and~4 will be carried
out by the postdoc. The time table below summarizes how the PhD student and the
postdoc will contribute to each task. In practice, the research will likely be
more interwoven than shown in the table. It can be beneficial for a researcher
to switch frequently between two tasks and to use the insights gained on one
task when carrying out the other task. Moreover, interweaving makes it easier
to incorporate the lessons learned in Tasks 3~and~4 when carrying out Tasks
1~and~2, and vice versa.\strut

\vspace*{-.5\baselineskip}

\begin{center}
\includegraphics[scale=.35]{diagrams/time-table}
\end{center}

\beforepara
\paragraph{Task 1: Develop and deploy Aesop.}

Aesop normally performs backward reasoning; that is, it reduces proof goals to
a set of subgoals, working from conclusions towards premises. In this task, we
will develop support for forward reasoning---the derivation of new hypotheses
from existing hypotheses. In practice, some goals are easier to prove following
forward steps than backward steps. For example, in the theory of Diophantine
equations, detailed case analyses lead to many hypotheses; from these,
forward reasoning can derive new, useful hypotheses.
%
A combination of forward and backward reasoning is often beneficial.
Some basic support for forward reasoning is already included in Aesop,
% (in the form of \texttt{forward} and \texttt{destruct} rules),
but it is highly inefficient and cannot be used to its full potential. We will
investigate how to automatically derive longer chains of forward reasoning,
motivated by our application to Diophantine equations.

\looseness=-1
A forward-reasoning Aesop will \emph{saturate} the
hypotheses present in the current goal---that is, systematically derive new
hypotheses from existing ones using specially tagged \texttt{forward} and
\texttt{destruct} rules.
%
To support this efficiently, we propose to design a data structure that will
store the current hypotheses as well as the set of \texttt{forward} lemma
hypotheses that can be discharged using the current hypotheses. We aim to
design the data structure so that it will grow monotonically as new hypotheses
emerge in the goal. In this way, expensive recomputation of information will be
avoided.
%
%Because Aesop will be optimized to work with
%forward rules, users will be able to register more rules as forward, increasing
%its power.

\looseness=-1
For example, suppose there is a \texttt{forward} lemma with
$h_1,\dots,h_{10}$ as its hypotheses and $c$ as its conclusion, and the goal
has $h_1$ among its hypotheses. The current Aesop will try to discharge the
lemma's hypotheses, but it will fail if $h_2,\dots,h_{10}$ are missing
in the current context. If, however, $h_2$ emerges, then Aesop will try
again to apply the lemma. This dance will continue as $h_3, \dots, h_{10}$ are
derived, and only then will $c$ be derived and added as a hypothesis. This
example is simplistic, since the hypotheses in the context are identical to
the lemma's hypotheses and the correspondence between the hypotheses is
obvious, but in general expensive unification needs to be performed to localize
the lemma's hypotheses among the current goal's hypotheses. Another
difficulty is that several of the goal's hypotheses may unify with the same
hypothesis of the lemma, slowing down the dance even more.

An important part of this task will be to use Aesop ourselves on the Lean
theories developed as part of this project, as a case study guiding Aesop's
development. We will employ Aesop extensively on our proof developments, as a
terminal tactic in one-line subproofs within larger Mizar-like declarative
proofs. We will fine-tune its setup for both basic Lean modules %(e.g., sets)
and modules related to Diophantine equations.
%Finally, we will assess
%its strengths and weaknesses in the context of Diophantine equations and use
%this assessment to guide further development.

\beforepara
\paragraph{Task 2: Develop, apply, and optimize Lean-auto.}

The first hammers worked with simple type theory (higher-order logic). The
deeper scientific question here is how to encode dependent type theory in
higher-order logic to exploit automatic provers. CoqHammer has shown that
hammers can in principle be designed to support with the more expressive
dependent type theory, but more research is necessary to obtain high success
rates in practice. In collaboration with Avigad's team at CMU, we will resume
and complete the development of Lean-auto.

\looseness=-1
We will base our translation on Cruanes and Blanchette's ideas
\cite{cruanes-blanchette-2016}. The main advantage of this translation---%
which was designed to find counterexamples, not proofs---is that
it locally encodes any dependent type feature, avoiding clutter. We expect that
it can be extended and that first- and higher-order provers can
actually provide strong automation for dependently typed theory.
%
Consider the type class of monoids, which
bundles an element $e$, a binary operation $\mathit{op}$, and the properties
$\mathit{left\_neutral} : \forall x{,}\; \mathit{op}\; e\; x = x$,
$\mathit{right\_neutral} : \forall x{,}\; \mathit{op}\; x\; e = x$, and
$\mathit{assoc} : \forall x\, y\, z{,}\; \mathit{op}\;(\mathit{op}\; x\; y)\; z =
  \mathit{op}\; x\; (\mathit{op}\; y\; z)$.
%
An optimized translation would map
instances of monoids as pairs $(e, \mathit{op})$ on which the predicates
described by $\mathit{left\_neutral}$, $\mathit{right\_neutral}$,
and $\mathit{assoc}$ are required to hold.
%
Another promising avenue, which is already partly implemented in Lean-auto, is
to heuristically instantiate types and type classes in generic lemmas in the
context \cite{clune-et-al-2024}. This process is called \emph{monomorphization}
and has been used very successfully for encoding Isabelle's
polymorphism \cite{blanchette-et-al-2016-types}. The challenge is to cope with
Lean's much more expressive type system, which allows higher-rank polymorphism,
whereas in Isabelle polymorphism is rank-1. We aim to identify a large fragment
of Lean's logic where polymorphism can be efficiently eliminated by
monomorphization and will encode the remaining polymorphism using other
techniques.

%Like for Task 1,
An important part of this task will be to use Lean-auto on
the Lean theories developed in Task~4. %, as a case study.

\beforepara
\paragraph{Task 3: Define and verify computations related to Diophantine equations in Lean.}

\looseness=-1
%The use of effective methods for explicitly resolving Diophantine equations is a central and vast field with various techniques.
On the Diophantine front, we aim to start by formalizing computations concerning the arithmetic of number fields $K$, i.e., finite field extensions of the rational numbers $\Q$.
%Examples of which are $K_1=\Q(i)=\{a+b i \mid a,b \in \Q\}$ where $i:=\sqrt{-1}$, or $K_2=\Q(\alpha)=\{a+b\alpha+c\alpha^2 \mid a,b,c \in \Q\}$ where $\alpha$ is is the (say) real number satisfying $\alpha^3+2 \alpha-1=0$.
%
Basic aims include computing
the \emph{class group} $\operatorname{Cl}_K:=\operatorname{Pic}(\mathcal{O}_K)$ and the \emph{unit group} $U_K:=\mathcal{O}_K^*$
of
the \emph{ring of integers} $\mathcal{O}_K$; see, e.g., Cohen \cite[Chapters 4 and 6]{cohen-1993}.
Further arithmetic invariants, including generalizations such as general orders in number fields, $S$-units, and $S$-class groups,
%(for a finite set op prime ideals $S$ of $\mathcal{O}_K$), as well as analogues for function fields,
might be considered, depending on the details of the Diophantine problems encountered in Task~4.
%For efficiency reasons, it may also be desirable to establish suitable certificates for derived objects, such as a system of representatives in $U_K$ for the quotient $U_K/U_K^m$ for some fixed integer %$m>1$.
%%, again depending on the specific Diophantine applications.
In previous work~\cite{baanen-et-al-2021}, initiated by Dahmen and
Anne Baanen (a former PhD student supervised by both applicants), rings of integers of number fields $\mathcal{O}_K$ (or more generally global fields) and their class groups were formalized together with some of their fundamental properties, like $\mathcal{O}_K$ being a Dedekind domain and the finiteness of $\operatorname{Cl}_K$.
As a next step, we will make such objects amenable to computations in Lean.
While \texttt{mathlib} is mainly developed using nonconstructive logic, this does not hinder us from computing with these objects in a tactic.
This works as long as care is taken in choosing a suitable computational representation for these objects.
For example, we could represent an ideal in a Noetherian ring $R$ simply by a finite set (or list) of generators;
recursively, we would then need to choose suitable representations for the generators, depending on $R$.

%interesting to develop new mathematics around these reps.+ finding appropriate reps 

\looseness=-1
As a case study~\cite{baanen-et-al-2023},
%Dahmen's team
Baanen, Dahmen, and the former postdocs in Dahmen's team
recently carried out the first nontrivial class group computations in Lean---e.g., ${|}\!\operatorname{Cl}_{\Q(\sqrt{-5})}\!{|}=2$.
%For example, computing $\operatorname{Cl}_K$ for $K=\Q(\sqrt{-5})$, in particular getting $|\operatorname{Cl}_K|=2$.
%We note that this is done without using specific tools for quadratic fields (like quadratic forms, though this specific approach would be interesting in its own right), making use of some effective geometry of numbers arguments.
While this illustrates in principle the feasibility of nontrivial class group computations in Lean, much work remains to scale this up.
%to number fields of larger degree, or even just quadratic number fields of somewhat larger absolute discriminant.
To this end, we will establish efficient underlying computations, involving ideal multiplication, prime ideal testing, and principal ideal testing.
%
%
While there are perfectly good algorithms available for all these items (see, e.g., Cohen \cite[Algorithm 6.5.10]{cohen-1993} for principal ideal testing), we are mostly interested in verifying certificates for the more involved computations.
Similarly, we will investigate certificates for computing $U_K$, etc.
%the ring of integers $\mathcal{O}_K$
%(say given through an integral basis)
%and its unit groups $U_K$.
%(say given by a system of fundamental units and a torsion generator). 
%
Establishing suitable certificates in the context of Lean, where we have to balance classical complexity issues with representations in Lean's dependent type system, will be part of the main research questions.
As we have to efficiently carry out (usually repeatedly) the computation for verifying an instance of the certificate, as well as prove the correctness of the verification procedure for the certificate.
%This also applies to the certifications mentioned later. 
 %Prime ideal testing, OK given the fundamental equality + norm computation and prime factorizaton (in Z and ring of integers)
 % For principal ideal testing, see Cohen, but note different certificates (classical complexity issues together with representation in dependent type system), or use (sometimes), e.g., Hasse norm theorem

%Coming back to computing the ring of integers $\mathcal{O}_K$, a suitable certification will likely involve checking $p$-maximality of $\mathcal{O}_K$ for all primes $p$ dividing its discriminant (or actually just for $p^2$ dividing it).
%What the most suitable representations in Lean of $\mathcal{O}_K$ for the various computational tasks inside $\mathcal{O}_K$ should be, remains to be determined; considerations may vary from storing a multiplication table for an integral basis of $\mathcal{O}_K$, to working directly with a defining polynomial for $K$ and considering $\mathcal{O}_K$ as a subtype of $K$.

%Other essential computations involve computing the unit groups $U_K$.
%Dirichlet's unit theorem~\cite[Theorem 7.4]{neukirch-1999} has recently been formalized in Lean, but again, linking it to the desirable computations is far away.
%Certification of an explicitly given system of fundamental units (and the torsion subgroup, but that is easy) in $U_K$ will be considered.
%For many Diophantine applications only a complete system of representatives in $U_K$ for the quotient $U_K/U_K^m$ for some fixed integer $m>1$ needs to be considered.
%For efficiency reasons it is also desirable to establish suitable certificates for such quotients directly as well.
%
%Of course, there are various interesting generalizations, such as dealing with general orders in number fields, $S$-units and $S$-class groups (for a finite set op prime ideals $S$ of $\mathcal{O}_K$),
%as well as analogues for function fields. Especially $S$-units will be relevant in a Diophantine setting.

%\looseness=-1
To produce certificates, we consider using a computer algebra system, such as SageMath~\cite{sagemath}.
Transferring externally computed certificates to Lean, could be done manually in an ad hoc fashion, but a more robust and sustainable approach will be to build on the prototype integration of SageMath in Lean \cite[Section 7 and appendices]{baanen-et-al-2023}.
%Connected to this is the formal irrationality proof of $\zeta(3)$~\cite{mahboubi-sibut-pinote-2021}, involving Assia Mahboubi (who is a guest professor at VU Amsterdam),
%where Maple scripts were used to produce input for the proof assistant Coq.
We will also consider producing certificates directly by tactics inside Lean, especially for the less involved algorithms.
% and/or the more complex/long outputted certificates.
%In desirable cases,
%especially for repeated ``small'' symbolic computational tasks,
%a more lightweight
%%and robust
%alternative is to develop complete computer-algebra-style
%tactics directly in Lean, dealing with the complete calculation at once.

%Some such tactics are already included in \texttt{mathlib}.
%As one example among many, \texttt{ring\_exp}, which was developed by Anne
%Baanen, one of our PhD students in Amsterdam, was designed to normalize
%expressions over rings, gracefully coping with variables in exponents.
%It can prove formulas such as $2^{n+1} - 1 = 2\cdot 2^n - 1$ and $(a + b)^{n +
%2} = (a^2 + b^2 + a\cdot b + b\cdot a)\cdot (a + b)^n$ fully automatically.
%Similar (but more ``easy'') tactics could be developed for repeated small computational tasks. 
%In this task, we will design and implement new algorithms for manipulating proof goals conveniently.

Following a similar approach, next targets could include the following:\
(1) developing flexible statements for checking obstructions to existence of solutions to (integral and rational) Diophantine equations, directly locally (both in a mod $p^n$ and $p$-adic language), as well as derived from reciprocity;
(2) extending continued fractions computations, as well as establishing (basic) lower bounds for linear forms in logarithms~\cite{smart-1998}, at least first in the Archimedean case
and later on also in the non-Archimedean case if desired for the Diophantine applications.

%Mention examples (incl. own) also ``cursed curve''; see foo, or, for a more popular account, bar..
%We will focus on a range of number theoretic data, central to the resolutions of various interesting Diophantine equations as described in Key objective 4 below.
%Such number theoretic data includes 
%
% building the basics with already interesting applications

%We will mainly cover computations related to some essential algebraic number theory, involving continued fractions, rings of integers, class groups, unit groups, local obstructions, etc.
%\begin{itemize}
%\item continued fractions
%\item algebraic number theory (rings of integers, class groups, unit groups)
%\item linear forms in logarithm
%\item local obstruction (including effective lifting lemmas)
%\item $p$-adic techniques.
%\end{itemize}

%Computer algebra systems are used to carry out computations in all kinds of
%contexts. Users are often applied mathematicians, but even pure mathematicians
%depends on computer algebra (e.g., for proofs of modularity \cite{xxx}).

%Computer algebra systems offer a vast collection of algorithms.
%The main difficulty is to obtain and reconstruct certificates produced by the algebra systems, to
%validate the results in the proof assistant.
%Fortunately, for many algorithms (e.g., lattice reduction), the answers are
%their own certificates.
%We plan to expand the Lean--Mathematica bridge \cite{lewis-wu-2022} to cover more algorithms.

%Roughly speaking the computations fall into four categories:
%\begin{enumerate}
%\item\label{item-reflection} The underlying algorithms, including proofs of correctness, are fully formalized. So the computation can be done inside the kernel and the outcome is formally verified by design.todo: mention "reflection"?
%\item\label{item-build} There is a \emph{tactic} attempting to performing the computation and building up the proof of correctness for this instance simultaneously. There might not be an a priori (unformalized) guarantee that the tactic produces a correct result, but when it finishes with a computation and accompanying proof term, the correctness is formally verified 
%\item A \emph{tactic} produces the data together with a (short) certificate. Then~\ref{item-reflection} and~~\ref{item-build}.
%\item An external tool (computer algebra system) produces the data together with a (short) certificate. Then~\ref{item-reflection} and~~\ref{item-build}.
%\end{enumerate}
%In practice, hybrid combinations could be used.
%For the more involved computation we will aim at resorting to the last two options, especially the final one whenever possible ****\\

\beforepara
\paragraph{Task 4: Design and develop a Lean library for Diophantine equations.}

\looseness=-1
For classical equations, including Mordell's equation~\eqref{eqn Mordell} and other superelliptic equations (over the integers), we will tackle the research problem of establishing the range of parameter choices that can be supported in a fully formalized setting,
and push the range as far as possible.
For example, we aim at establishing a first ``large'' bound $C$ for which Mordell's equation~\eqref{eqn Mordell} for all $|D| \leq C$ will be resolved in Lean.
%Concerning resolving classical equations like Mordell's equation~\eqref{eqn Mordell} for $|D| \leq C$, it is a research questions to establish (and push) what values of $C$ is ``reasonable'' in a fully formalized setting.
%As a modest initial goal one could, e.g., take $C=25$.\footnote{For a list of solution (with notation $n$ instead of $D$) see \url{https://en.wikipedia.org/wiki/Mordell_curve\#List_of_solutions}\,.}
%Though in fact, due to the nature of Diophantine equations, there is no ``smooth'' dependence of the solutions on $D$. The ease of resolution might depend heavily on arithmetic properties of $D$, such as whether or not the class number of the number field $\Q(\sqrt{D})$ is divisible by $3$ (noting that if $D$ is a square, resolution becomes very easy).
This will involve testing and optimizing the methods from Task 3 for computing class and unit groups, combined with basic (integral) descent methods, and solving (genuine) cubic Thue equations when $D<0$.
To resolve Thue equations in general, we will employ methods from lower bounds for linear forms in logarithms---initially following Bilu and Hanrot's method~\cite[Section~VII.3]{smart-1998} \cite{Bilu-Hanrot-1996}.
A natural continuation will be to resolve Thue--Mahler equations---initially following Tzanakis and De Weger's method~\cite[Chapter~VIII]{smart-1998} \cite{Tzanakis-deWeger-1992}---and apply this, e.g., to tabulating rational elliptic curves with prescribed bad reduction.

\looseness=-1
For the generalized superelliptic equations, we will build on the aforementioned methods, possibly enlarging the descent techniques, including Best et al.~\cite{Best-et-al-2023}.
Specifically, for the generalized Fermat equation with prime exponents $p=q\not=r$, a unit group sieve could be employed \cite[Section 4]{Dahmen-Siksek-2014} \cite[Section 7]{BCDDF-2023}.
This could take care of many tedious case distinctions and would explicitly reduce resolving the equations to finding rational points on finitely many hyperelliptic curves.
In principle, explicit descent for (hyperelliptic) genus $\geq 2$ curves should be employable in Lean, say, via first computing 2-Selmer groups of their Jacobians.
It seems, however, more reasonable to first focus on elliptic curve quotients of rank 0, and hence employ descent on elliptic curves, building on the %nice
recent group law formalization~\cite{Angdinata-XU-2023}.

\looseness=-1
Finally, other new Diophantine results that might benefit from the formal setting, include
(1)~resolving multi-parameter families of Diophantine equations where the underlying (computational) invariants will take on only finitely many different values upon varying the parameters,
%(for which restrictions such as bounds and congruences may apply)
e.g., some infinite families of superelliptic equations;
(2)~determining small powers in a wide variety of elliptic divisibility sequences.
What exactly will be possible remains to be explored and will heavily depend on the precise progress of the previous parts, particularly on the available proof automation.

\subsection{Justification}
% Discuss the choice for the type of personnel (e.g. PhD and/or post-doc) and possibly non-scientific staff. Refrain from giving the name of the intended personnel in so far as you already have a candidate in mind.
%Also discuss and motivate your choices for budget decisions. Provide a justification for the budget for knowledge utilization, internationalisation, Money follows Cooperation, and a motivation for an excess in materials budget (if the cumulative total exceeds more than k€ 15 per scientific position per year). 
%In case a small investment (up to € 150,000) is foreseen, indicate whether this investment will be developed exclusively for the proposed research, why there is no nearby equipment available that warrants this investment and how the investment relates to the number of researchers using it.
%When filling out the budget table be aware of the following: 
% *costs for Open Access publishing should be included under ‘Materials/Implementation costs’, 
% *travel and accommodations costs for the scientific positions applied for should be included under ‘Materials/Travel and accommodation costs’. 
% *Travel and accommodation costs in so far as these concern direct research costs emerging from the international collaboration of PI’s should be included under the module ‘Internationalisation’. 
% *When applying for budget under the module 'Money follows cooperation' the foreign researcher should be the co-applicant and funding is requested for a scientific position (PhD or Postdoc) abord; please see the Call for Proposals for more information and requirements, or contact NWO.

\medskip

\looseness=-1
The personnel costs, amounting to $386\,707$\euro{} (including bench fee),
consist of hiring a postdoc full-time for four years. The postdoc will work at
VU Amsterdam and will focus on the mathematical side of the project, namely,
Tasks 3~and~4. We expect these tasks to be the most difficult ones, because
they involve advanced mathematical challenges while requiring expertise with a
proof assistant.
%
In addition, via the Money follows Cooperation scheme, a PhD student will work
at LMU München and will focus on the computer science side of the project,
namely, Tasks 1~and~2. We expect these tasks to be suitable topics for a PhD
student. Munich is an ideal place to carry out this research due to the
presence of local expertise with Aesop and hammers.
Blanchette and his team will contribute specific expertise to the research
project that is not available in the Netherlands at the level necessary for the
project (Section~\ref{ssec:embedding}).

% Will be about 624k\euro (including bench fee)

Travel and accommodation costs will arise from participations to conferences,
mutual visits of the two teams, and visits to other researchers. We budget
4k\euro{} per year per hired staff (in addition to the bench fee). The mutual
visits will be invaluable to strengthen the ties between the two teams
distributed over two countries.

The material costs amount to 35k\euro.
Travel and accommodation costs for the postdoc are described above (16k\euro). The implementation costs (19k\euro) include open access publishing (5k\euro).
We do not expect prohibitively high costs for open access because we will generally prefer venues that publish open access by default.
%Although we will prefer venues
%that publish open access by default, this might not always be the best option
%to reach the desired audience.
The implementation costs also include two meetings involving the VU and LMU teams and selected other scientists (14k\euro, 7k\euro{} each).
These meetings will consist of a small-scale workshop week, culminating in a day long seminar at the end for a broader scientific audience (in the style of an ``Intercity Number Theory Seminar'', as organized in the past by Dahmen).

We also have costs of $277\,220$\euro{} associated with Money follows Cooperation.
The main costs are personnel costs ($261\,220$\euro{}, corresponding to $0.891
\times 287\,565+5\,000$, rounded, including bench fee), for
hiring one PhD student for four years full-time at LMU München; we budget 16k\euro{} travel and accommodation costs for the PhD student.

Finally, we have internationalization costs of 25k\euro{} for organizing an international workshop (15k\euro) as well as inviting guest researchers throughout the project (10k\euro, 2k\euro{} per year).

\subsection{Embedding of research and relevant expertise of researchers involved}
\label{ssec:embedding}
% Describe how the proposed research fits with the participating researcher(s) and indicate how the proposed research fits within the (inter)national science landscape. If applicable, you may wish to use the suggested headings.

%Expertise
%
% Describe the expertise of the applicant, but refrain from including an extensive CV. Hence, you are instructed to only list relevant information regarding expertise without describing a full track record. 
% *Additionally, you may not mention lists or total numbers of prizes, grants, total acquired sum of funding, publications or supervised PhDs/PDs. 
% *Furthermore, you may not list personal grants, such a grants from NWO's Talent Programme. 
% *You may describe ongoing work in your lab and you are allowed to refer to consortia that you are part of. However, in case you mention specific consortia grants or (prestigious) prizes, you must provide context, i.e. by describing how the current proposal follows up on previous work, how there is synergy between the current proposal and ongoing project(s)/programme(s) or how the network of another programme is relevant to the current proposal. 
% *You may include references to publications showing previous work. However, be consistent in using the same reference format throughout the proposal.
%Remember to comply with DORA, i.e. do not use quality indicators that are measured on the author or journal level (for more information on DORA see p.1).

%If applicable
%Collaborators
%
%Describe how the proposed research will benefit from local, national and/or international collaborations. Please refrain from referring to reputation of the collaborators, e.g. do not mention terms as ‘leading institution’ or ‘world renowned scholar’, but instead provide substantiation of relevant qualities and expertise that will benefit the research. You may include references to joint publications with collaborators, to show a successful past/ongoing collaboration. However, be consistent in using the same reference format throughout the proposal.

%If applicable
%Infrastructure
%
%Describe how you have access to the required equipment locally or to larger national or international infrastructures; this may also include digital infrastructure such as access to computational resources or databases.

\medskip

\looseness=-1
Both the field of Diophantine equations and that of formal theorem proving are
of central interest in the Netherlands and worldwide. In the Netherlands,
formalization research occurs in, e.g., Amsterdam (CWI, UvA, VU), Delft, Nijmegen,
and Utrecht; Diophantine research occurs in, e.g., Amsterdam (UvA, VU), Groningen,
Leiden, and Utrecht.

\looseness=-1
The project will be hosted by the Department of Mathematics of
VU Amsterdam and the Department of Informatics of LMU München.
%
The project is the logical sequel to Dahmen's ``New Diophantine directions''
(2017--2022) and Blanchette's ``Lean forward:\ Usable computer-checked proofs and
computations for number theorists'' (2019--2023)---the first project is about
developing the theory of Diophantine equations, the second project is about
improving Lean and applying it to number theory. These projects have led to
substantial results, on which we can now build.

Dahmen's main expertise is in number theory,
with a clear track record tackling hard Diophantine problems (e.g., \cite{Bennett-Dahmen-2013, Dahmen-Siksek-2014, Bennett-et-al-2015, Dahmen-vLangen}).
Since 2017, he has also been active in research, teaching, and organization within the field of formalized mathematics, especially focussing on connections to number theory.
In particular, he has initiated research projects resulting in three publications about Lean formalizations \cite{dahmen-et-al-2019, baanen-et-al-2021, baanen-et-al-2023}.
Blanchette's experience is a unique
blend focusing on the automation of proof assistants and the development of
automatic theorem provers. He led the development of the automatic theorem
prover Zipperposition and of its underlying calculus, $\lambda$-superposition.
Zipperposition finished in first place in the higher-order theorem division of
the CADE ATP System Competition in 2020, 2021, and 2022.
% establishing itself as the leading automatic theorem prover for simple type theory.
His expertise with automatic theorem provers is invaluable both when designing
general-purpose automatic tactics such as Aesop and when integrating automatic
provers in hammers. Despite the presence of several theorem proving groups in
the Netherlands, Blanchette will contribute specific expertise regarding
white-box and hammer-style proof automation that is not available in the
Netherlands at the level necessary for the project.

Clearly, the collaboration between Dahmen and Blanchette corresponds to a need
and brings complementarity and added value. We have been collaborating since
2018. We have jointly supervised a PhD student who completed their thesis
with the prestigious \emph{cum laude} distinction and are jointly supervising a
second one. We also have organized regular Lean meetings, which attracted members of
both teams. We both have experience supervising several other PhD students %who
%completed their theses
as well as postdocs. The project will consolidate this
collaboration and help keep Blanchette's expertise directly
available to the Dutch research community. It will also benefit from both
researchers' extensive networks of collaborators in the fields of Diophantine
equations and formal theorem proving.

\looseness=-1
Both applicants have ample experience organizing events.
Recent activities of Dahmen %in this direction
include \hbox{(co)}\allowbreak organization of the international Lorentz Center workshop Machine-Checked Mathematics, % in July 2023, 
%the Imaginary Amsterdam math exhibition, % in May 2023,
the VU/Utrecht Informal Formalization Seminar,
and sessions of the national Intercity Number Theory Seminar. % in June 2023 and June 2022.
Blanchette (co)organized multiple conferences and workshops, including
the Interactive Theorem Proving conference and two Dagstuhl seminars on Deduction.

\looseness=-1
Moreover, we will closely synchronize with Assia Mahboubi (Inria Nantes), who
is a guest professor at VU Amsterdam and leads the %ERC
project
``FRESCO:\ Fast and reliable symbolic computation'' (2021--2026).
%about implementing computer algebra algorithms in the Coq proof assistant.
The
focus of our proposal is different, as we have a concrete objective in
mind---verified Diophantine equations---which will guide the choice of
algorithms to consider.
Nonetheless, our project will surely benefit from her
expertise and her team's experience.

Task~1 has ties to Blanchette's %NWO Vidi
project ``Lean forward''. This is the
project that funded most of the development of Aesop. For this task, we will
closely collaborate with Jannis Limperg, who is now at LMU München and expected
to continue as a postdoc at LMU after completing his PhD.
%
Task~2 has ties to Blanchette's %ERC
project
%``Matryoshka:\ Fast
%interactive verification through strong higher-order automation'' (2017--2022)
%and
``Nekoka: Realizing the Promise of Higher-Order SMT and Superposition for Interactive Verification'' (2023--2028).
We will build on Blanchette's network of collaborators,
including
Jeremy Avigad (CMU), a leading Lean user, and
Alexander Bentkamp (HHU Düsseldorf), who codesigned
$\lambda$-superposition and codeveloped Zipperposition and \verb|duper|.

\looseness=-1
Task~3 is related to a small project led by Dahmen, about formalizing number
theory, which partly funds a PhD student, Alain Chavarri Villarello (supervised by Dahmen and Mahboubi).
It provides some groundwork, like explicit formalized rings of integers for general degree.
%, who started in September 2022 under the joint supervision of Dahmen and Mahboubi.
Moreover,
for Task 3~and~4, we will collaborate with the \texttt{mathlib} community,
forming ``coalitions of the willing'' as we have done in the past
(e.g., the four-author ITP 2021 paper~\cite{baanen-et-al-2021}). %, likely involving Alex J. Best (KC London).
%Finally, the area of Diophantine equations is strongly represented in the Netherlands and also internationally of central interest.
%The postdoc will benefit from Dahmen's extensive contacts, including international renowned researchers like Mike Bennett (UBC).

\subsection{Risk assessment}
% Discuss feasibility of the research proposal and indicate the possible risks involved with the proposed research, including risks from the methods, techniques, available infrastructure, etc. Indicate how these risks can be mitigated and whether an alternative approach (plan B) exists.

\medskip

\looseness=-1
The various tasks can benefit substantially
from each other, but most of them do not crucially rely on each other.
The improvements to
Aesop and Lean-auto as part of Tasks 1 and 2 will help the formalization
work of Tasks 3~and~4, but without them formalization could still proceed,
albeit much slower. Conversely, the formalization work is expected to provide
invaluable case studies to guide the development of Aesop and Lean-auto,
but if necessary additional case studies could be considered.
Tasks 1 and 2 are largely independent. By contrast,
Task~4 will partly depend on Task~3;
the choice of Diophantine equations for Task~4 will determine on which parts of
Task 3 we will build.
In sum, although
each task carries its own risks, the project will be robust and adapt to
changing circumstances.

For Task 1, about Aesop, the main risk is that we might not be able to obtain
the desired performance to obtain a practically useful tool. Any tool based on
saturation can be highly explosive. We expect that our incremental data structure
will mitigate the explosion. In the unlikely event that forward reasoning turns
out to be impracticable, we would focus on carrying out a case study based on
Diophantine equations and improving Aesop based on that.

For Task 2, one danger is that Lean-auto might be too slow in practice.
%This
%was, in fact, the reason why we never succeeded at providing a hammer for Lean
%3.
Lean-auto's relevance filter needs to go through ten of thousands of lemmas,
and its monomorphizer needs to iterate multiple times through perhaps one
thousand lemmas. However, so far benchmarks indicate that we can iterate over
the entirety of the current \verb|mathlib| within a few seconds, which should
suffice for a hammer. Should performance be an issue, we would implement some
of the same kinds of optimizations that we coded in Sledgehammer.

\looseness=-1
For Task 3, apart from the ``pure'' formalization challenges,
to which the aspects mentioned in Task~4 below also apply to some extend,
a specific risk to consider would be that some generalizations would become too involved.
For example, if incorporating non-Archimedian linear forms in logarithm is too demanding,
%This would restrict the range of Diophantine applications in Task 4,
the Thue--Mahler equations in Task 4 will likely not be considered,
but instead there will be more focus on Thue equations and their applications.
%certificates could become too complicated in practice
%to port ad hoc from a computer algebra system to Lean.
%A potential remedy would be to spend more time on developing a robust bridge between the algebra system and Lean as needed.
%Another issue is that some computations in Lean itself would not be fast enough..

\looseness=-1
The task with the highest scientific risk is
Task~4, where all the threads %of the project
come together.
%Though we note that the chosen Diophantine equations under consideration will determine which parts from Task 3 are actually needed.
%The most risky
%aspect is perhaps best summarized by the motto `
Of course, interactive theorem proving
takes time, but a postdoctoral researcher with a four-year
contract should be able to make good progress.
% but it is notoriously hard to
% predict the speed of development of formal proofs.
%Nevertheless,
Our experience
in the past few years formalizing topics of number theory makes us confident
that the plans are realistic. This assumes that we find a suitably skilled
postdoc. Our joint international network should allow us to
attract strong candidates, as in the past
(e.g., Alex J. Best, Nirvana Coppola, Gabriel Ebner, Johannes Hölzl, and Robert Y. Lewis).
The task is open-ended; even a new formal library on only classical Diophantine results
would be valuable. %, though we hope for and expect more progress of course.

%Task 1 is fairly resilient because it considers independent improvements to
%\texttt{mathlib}. It could be carried out using Lean 3 or 4, as needed, but it
%would certainly benefit from the additional speed of Lean 4.

%In conclusion, the formalization of mathematics has a long history, especially
%in the Netherlands, starting with the pioneering work of Nicolaas De Bruijn.
%But only in the past few years have research mathematicians started to widely
%adopt proof assistants, with top mathematicians such as Peter Scholze and
%Terence Tao engaging with the field. Proof assistants are evolving fast and
%promising to become indispensable tools for future mathematicians. This project
%is very timely and will make a real difference. In addition to the PI and
%co-PI, it will involve two hired staff and several collaborators. Through
%workshops, publications, and our scientific network, we also expect the project
%to gain high visibility and attract further collaborators.

\newpage
\section{Scientific and/or societal impact}
% Section A.3 is limited to one page, including figures and tables and excluding literature references.

\medskip

Applicants in the Open Competition Domain Science – M can choose to put primary focus on scientific impact, societal impact, or a combination thereof. This application opts for: scientific impact.
%Choose scientific and/or societal impact.


% Explanatory Notes
% Select which kind of impact the proposal focusses on and motivate your choice. The applicant has the choice whether to focus on achieving scientific impact, societal impact, or a combination thereof. It is not necessary to include both types of impact to get a good score for this assessment criterion. A focus on scientific impact, a focus on societal impact, or a combination thereof, can lead to a good score, provided that it is well motivated. So, please motivate your choice and elaborate on all applicable parts of the criteria for the chosen form of impact (see call for proposals).

% Scientific impact is the impact of research on one's own research field, on related research fields or on the broader scientific community. The potential and relevance of research results for one’s own discipline and related discipline(s) and the potential and relevance of the research results for the wider scientific field form part of the assessment when a focus on scientific impact or a comparable focus for both scientific and societal impact is chosen.

% Societal impact can broadly be defined as any cultural, economic, industrial, environmental and/or societal change that is (in part) the result of the knowledge and skills acquired through the proposed research. The potential for societal impact in the short and long term and the vision of the way(s) in which the proposed research could lead to societal impact form part of the assessment when a focus on societal impact or a comparable focus for both scientific and societal impact is chosen.

% On the basis of the referee reports and the rebuttal, the committee will assess whether there are possibilities for impact that are not described in the proposal, and take this into account in its assessment.

\medskip

\noindent
The research is of a fundamental type. We expect the project to have primarily
scientific impact, concerning automation in proof assistants, libraries of
formalized mathematics, trustworthy computations, and number theory.

On the proof assistant front, our main contributions will be an improved Aesop
tactic and a highly usable Lean-auto with a high success rate. Such
productivity-increasing tools have been eagerly awaited by the entire Lean
community. Blanchette's work on Lean-auto's precursor Sledgehammer, which he
started 14~years ago, still has an impact on hundreds of users, many of whom
cannot imagine working without Sledgehammer. An even greater impact can be
expected for Lean-auto, given the size and remarkable growth of the Lean
community. As for Aesop, the extensions we have in mind should have an equally
important impact on the success rate of the tool, making Lean more accessible
to a broader range of users and making users---beginners and experts
alike---more productive.

General lessons learned from our project
will likely impact the field of theoretical computer science through improving
proof assistants and their tools.
% Many underlying methods also relevant for computational number theory in general 
% Some even more general (e.g., efficient linear algebra routines)
% So even has the potential to go beyond number theory
%
Very valuable will be the creation of reliable and reusable libraries of
formalized mathematics. These are expected to become increasingly important
within mathematics. Hence, the proposed research will also play
a significant role in the adaptation of proof assistants by the mathematical
community.

%Whereas Lean-auto will provide general-purpose proof automation, the
%computer-algebra-style tactics we plan to develop as part of Task~3 will have
%perhaps a more important impact on a more restricted class of users:\ number
%theorists.

Mathematicians relying on computer computations for their proofs might find the
substantial increased trustworthiness of our approach appealing to confirm results found
using traditional computer algebra systems. Moreover, the work on integrating
these systems will yield a better understanding of certificate production---a
contribution that is both scientifically rewarding and necessary for a
trustworthy integration.
%We expect the proposed research to impact not only number theorists but also
%mathematicians from other areas.
Although the project's focus will be to solve Diophantine equations, some of
the algorithms will have a wider scope of applicability; for example, some
efficient linear algebra will need to be developed. At the same time, the
computational aspect of the project will serve as a case study on formalized
computations inside a proof assistant.

\looseness=-1
Diophantine equations play a central role in modern number theory.
Therefore, the proposed research could have direct impact on the field of number theory.
The topic has many connections to other branches of mathematics.
Most notably to algebraic geometry, through the geometric viewpoint of integral and rational points on algebraic varieties,
and commutative algebra (both with and without this viewpoint),
but also for example to combinatorics, optimalization, and logic.
Especially the merits of the newly created formal libraries are expected to impact neighboring fields.

\looseness=-1
The research will be an interesting case study for the use of proof
assistants in modern mathematical research.
%, with a potentially revolutionary impact on the daily work of mathematicians.
A potentially extremely rewarding
long-term impact is that it will bring us closer to the day when proof
assistant will be used routinely to develop new mathematics. This would revolutionize the
way mathematics is created, with a rippling effect all over science. There
might also be a transformational impact in the review process of scientific
papers. Indeed, with work such as ours comes the long-term hope of a review process that
eliminates mistakes, discharging humans from the burden to check proofs in
detail. This would have a positive impact on both science and society.

Although the research is of a fundamental type,
we expect further societal impact.
One of the most appealing aspects of
Diophantine equations is that the main problems can easily be stated and
understood by someone with only some basic knowledge of %, say,
high-school mathematics. Therefore, new explicit research results in this area
are ideally suited for mathematics outreach and can show society that
mathematical research is very much alive today.
Dahmen has done this in the past on
many occasions (e.g., through presentations for high school students or
teachers and publications in popular scientific magazines) and will continue to
do this. Moreover, formalization as a topic will also lend itself to outreach.
%
Another societal impact of our work is that not only academic users of proof
assistant technology but also industrial users will benefit from stronger proof
automation. As a result, formal verification will become a more viable option
in industry.
Finally, the underlying computational aspects could in the long term %possibly
contribute to technology, especially in cryptography.

In conclusion, the formalization of mathematics has a long history, especially
in the Netherlands, starting with the pioneering work of Nicolaas De Bruijn.
But only in the past few years have research mathematicians started to widely
adopt proof assistants, with top mathematicians such as Peter Scholze and
Terence Tao engaging with the field. Proof assistants are evolving fast and
promising to become indispensable tools for future mathematicians and related
professionals. This project is very timely and contains all the necessary
aspects to make a real difference.


% If and how this will happen is
% very hard to predict at this point, as is the case for most fundamental
% research.


% Explanatory Notes
% The applicant has the choice whether to focus on achieving scientific impact, societal impact, or a combination thereof. It is not
% necessary to include both types of impact to get a good score for this assessment criterion. A focus on
% scientific impact, a focus on societal impact, or a combination thereof, can lead to a good score, provided that it is well motivated.
% So, please motivate your choice and elaborate on all applicable parts of the criteria for the chosen form of impact (see call for proposals).

% Scientific impact is the impact of research on one's own research field, on related research fields or on the broader scientific
% community. The potential and relevance of research results for one’s own discipline and related discipline(s) and the potential
% and relevance of the research results for the wider scientific field form part of the assessment when a focus on scientific impact
% or a comparable focus for both scientific and societal impact is chosen.

% Societal impact can broadly be defined as any cultural, economic, industrial, environmental and/or societal change that is
% (in part) the result of the knowledge and skills acquired through the proposed research. The potential for societal impact
% in the short and long term and the vision of the way(s) in which the proposed research could lead to societal impact form
% part of the assessment when a focus on societal impact or a comparable focus for both scientific and societal impact is chosen.

% On the basis of the referee reports and the rebuttal, the committee will assess whether there are possibilities for impact that
% are not described in the proposal, and take this into account in its assessment.

\newpage
\section{Literature/references} % (in this proposal)
% The list of references should be relevant to the research proposal, cited in the texts of sections A.2 and A.3. Be consistent in using the same reference format throughout the proposal and only include 'open literature'. It should not include internal documents (such as master theses) nor should it be a mere list of publications of the main applicant. If possible, you are strongly encouraged to include a DOI. This section does not count toward the page limitations.

\medskip

% EXAMPLE: Using bibtex
\bibliographystyle{unsrt}
\bibliography{application}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\part{Applicants and additional information}

\section{Research areas}
% Include at least one and at most five Domain Science research areas applicable to your research proposal. The list of admissible research areas can be found in section 7.1 of the call for proposals, round 2021-2022. Please indicate for each chosen research area (in percentages) the relevance to your research proposal. Use increments of 5%. The minimum percentage can be 20% and the sum of percentages should not exceed 100%. By using percentages, rather than a ranking of research areas, you can also indicate that
% some research areas contribute equally to your proposal. For example:
% - Stars (25%)
% - Inorganic chemistry (25%)
% - Geophysics (50%)
% Please note that these research areas do not correspond to the discipline codes asked for when submitting your proposal through NWO's online application system ISAAC. The research areas listed in this proposal (submitted as pdf) are used for further assessment of your application (e.g., the distribution of the proposal among the different cluster committees); the codes in ISAAC are not used for any such purpose. Please only supply the main discipline in ISAAC.

\medskip

\begin{itemize}
\item Algebra, number theory, discrete mathematics (50\%)
\item Logic, set theory (25\%)
\item Software engineering, programming languages, formal methods (25\%)
%\item Algorithms, data structures, complexity, and computability (20\%)
\end{itemize}

\section{Main applicant---additional information}
% NWO corresponds with you via email. Please, make sure that your email address at work is listed correctly in your profile in ISAAC. Tip: check your spam filter regularly as it might happen that an NWO email ends up there. NWO accepts no liability in case emails end up in the spam filter/box.

\medskip

% This is new table environment with only two columns, whose width can be specified
\begin{texttable}{7cm}{10cm}
  Name: % (titles, initials, first name, last name):
    & dr.\ S.R. (Sander) Dahmen \\ % Copy from A.1
  Affiliation: % (university/institute + department):
    & Vrije Universiteit Amsterdam \\
    & Department of Mathematics \\ % Copy from A.1
  Position: & associate professor \\ % Choose: professor / associate professor / assistant professor / other (specify)
  Paid position: & yes \\ % Choose: yes / no
  Type of contract: & permanent \\ % Choose: tenure track / permanent 
  End date of contract: & N/A \\ % Fill out: N/A or dd-mm-yyyy (provide a statement on guidance when your contract does not cover the runtime of the project in case of tenure track or upcoming retirement)
%  Full time or part time: & full time (1.0 FTE) \\ % Choose: full time / part time (1.0/0.8/... fte)
\end{texttable}

% This is new table environment with only two columns, whose width can be specified
\textbf{Co-applicant---additional information}

\medskip

\begin{texttable}{7cm}{10cm}
  Name: % (titles, initials, first name, last name)
    & prof.\ dr.\ J.C. (Jasmin) Blanchette \\ % Copy from A.1
  Affiliation: % (university/institute + department):
    & Ludwig-Maximilians-Universität (LMU) München \\
    & Institute for Informatics \\ % Copy from A.1
  Position: & professor \\ % Choose: professor / associate professor / assistant professor / other (specify)
  Paid position: & yes \\ % Choose: yes / no
  Type of contract: & permanent \\ % Choose: tenure track / permanent 
  End date of contract: & N/A \\ % Fill out: N/A or dd-mm-yyyy (provide a statement on guidance when your contract does not cover the runtime of the project in case of tenure track or upcoming retirement)
%  Full time or part time: & full time (1.0 FTE) \\ % Choose: full time / part time (1.0/0.8/... fte)
\end{texttable}

\section{Other pending or future grant applications on the same research topic}

\medskip

Yes
% If yes, please indicate below each proposal on the same research topic as the current proposal (to be) submitted to NWO or other funding agencies by you or by members of your research group. Describe the difference (give a percentage) of the current proposal with the other proposals. Running grants do not need to be reported. Please bear in mind that NWO does not fund the same/similar research twice. Copy and paste the table as often as needed.

\medskip

% This is new table environment with only two columns, whose width can be specified
\begin{texttable}{7cm}{10cm}
  Title proposal: & Towards formalized Diophantine research: bridging the gap\\
  Applicant(s): & dr.\ S.R. (Sander) Dahmen\\
  Funding agency and call: & NWO, Vici Grant\\
  Budget applied for: & $1\,500$ k\euro{}\\
  Date of submission: & 10 September 2024 (expected)\\
  Estimated date of decision: & 28 February 2025\\
  Difference with this proposal: & 80\% difference\\
  Describe difference: & Automation part is different, some overlap with Diophantine part\\
\end{texttable}

\section{Public summaries} % Also needs to be uploaded in ISAAC
% Include a short (max. 100 words) public summary both in Dutch AND in English with a catchy title, which NWO can use in press releases and on their website in case your research proposal gets granted.

%Dutch title and summary

%English title and summary

\medskip

Robuuste getaltheorie creëren met behulp van computers

\medskip

\noindent Wiskundigen zijn voor hun werk cruciaal afhankelijk van bewijzen en berekeningen, maar al te vaak bevatten hun bewijzen gebreken en de programma's die hun berekeningen uitvoeren fouten.
De oplossing voor deze problemen is het gebruik van speciale software, bewijsassistenten genaamd, om de bewijzen te controleren en de berekeningen te verifiëren.
Dit zal ook leiden tot waardevolle digitale wiskundige bibliotheken.
In dit project zullen we bewijsassistenten toepassen en uitbreiden om ze gemakkelijker te kunnen gebruiken voor een breed scala aan wiskundige toepassingen,
vooral gericht op één actief onderzochte tak van de getaltheorie: Diophantische vergelijkingen.

\bigskip

\noindent Creating robust number theory using computers

\medskip

\noindent Mathematicians rely crucially on proofs and computations for their work, yet too often their proofs are flawed
and the programs carrying out their computations are buggy.
The solution to these issues is to use dedicated software, called proof assistants, to check the proofs and verify the computations.
This will also lead to valuable digital mathematical libraries.
In this project, we will apply and extend proof assistants to make them more convenient to use for a broad range of mathematical applications,
focusing especially on one actively researched branch of number theory: Diophantine equations.
%The result will be tools and methodologies that can be used by number theorists
%and other mathematicians to check their own results.

\section{Questions Data management section}
% Explanatory Notes
% Responsible data management is part of good research. To promote effective and efficient data management,  data sharing and data reuse, NWO expects researchers to carefully manage data resulting from NWO-funded research and prospectively plan for which data will be preserved and shared.

% With the data management section, NWO mainly wants to raise awareness about the importance of responsible data management. The section is therefore not included in a committee's decision about whether or not a proposal should be awarded funding. NWO does, however, submit this section to the committee and referees for advice. 

% It is recommended that you seek advice from a data steward or research support office at your home institution to complete this section. They will be able to recommend suitable storage facilities and repositories for your data, and to advise on data management costs. After a proposal has been awarded funding, grantees are required to elaborate the data management section into a detailed data management plan explaining how research data and other results emerging from the NWO-funded research will be stored and made findable, accessible, interoperable and reusable (FAIR). 

% What does NWO understand as research data?
% Research data are the evidence that underpin the answer to research questions, and can be used to validate findings. Data can be quantitative information or qualitative statements collected by researchers in the course of their work by experimentation, observation, modelling, interview or other methods, or information derived from existing evidence. For the purpose of NWO's data management policy, the definition of research data does not include physical objects such as scientific and archaeological collections, physical arts works or biobanks; however, digital information extracted from such objects are to be regarded as research data. Software is also not included in the definition of research data. NWO recognizes that software (algorithms, scripts and code developed by researchers in the course of their work) may be necessary to access and interpret data. In such cases, the data management plan will be expected to address how information about such items will be made available.

% What data does NWO expects you share and preserve?
% Research results should be stored in such a way that they can be retrieved and reused in the long term, also by researchers in disciplines and organisations other than those in which the research took place. The operating principle is that all stored data are, in principle, freely accessible and that access is only limited if needed for reasons such as privacy, public security, ethical restrictions, property rights and commercial interests. 
% NWO expects researchers to preserve the data resulting from their projects for at least ten years, unless legal provisions or discipline-specific guidelines dictate otherwise. As much as possible, research data should be made publicly available for reuse, unless there are valid reasons not to do so. As a minimum, NWO requires that the data underpinning research papers should be made available at the time of the article's publication. Any tools or software (algorithms, scripts and code developed by researchers in the course of their work) necessary to access and interpret data should be made available alongside the data.

% The costs of data management are eligible for funding and should be included in the project budget. 
% Important factors that determine the costs are: 
% * the type of data; 
% * the capacity needed for storage and backup; 
% * the amount of work needed to allocate metadata and the compilation of other documentation such as codebooks and the queries used in the statistical package; 
% * the extent to which the data needs to be protected; 
% * the hiring in of external data management expertise or other expertise.


\begin{enumerate}[align=left,labelindent=0pt,labelsep=!,itemindent=0pt,labelwidth=1em]
\item Will this project involve re-using existing research data?\\ % to check box use $\boxtimes$
$\boxtimes$ Yes: From my own or a collaborator's prior research.\\ % to check box use $\boxtimes$
$\boxtimes$ Yes: Publicly available data.\\ % to check box use $\boxtimes$
$\square$ No: Have you considered re-using existing data but discarded the possibility? Why? % to check box use $\boxtimes$
% If no, please briefly explain why; if yes, state any constraints on re-use of existing data if there are any.  

\item Will data be collected or generated that are suitable for reuse? \\ % to check box use $\boxtimes$
$\boxtimes$ Yes: Please answer questions 3 and 4.\\ % to check box use $\boxtimes$
$\square$ No: Please explain why the research will not result in reusable data or in data that cannot be stored or data that for other reasons are not relevant for reuse. 

\item After the project has been completed, how will the data be stored for the long-term and made available for the use by third parties? Are there possible restrictions to data sharing or embargo reasons? Please state these here.

Our verified proofs and certified algorithms will become
part of \texttt{mathlib}, an open source library of verified mathematics located
on GitHub and maintained by the active \texttt{mathlib} community.
The Aesop tactic and Lean-auto will be available in separate public
repositories accessible to all Lean users. We will use very permissive open
source licenses for all our work.

\item Will any costs (financial and time) related to data management and sharing/preservation be incurred?\\ % to check box use $\boxtimes$
$\square$ Yes: Then please be sure to specify the associated expenses as ‘implementation cost’ within the budget post ‘Material costs’ in the budget table of this proposal.\\ % to check box use $\boxtimes$
$\boxtimes$ No: All the necessary resources (financial and time) to store and prepare data for sharing/preservation are or will be available at no extra cost. % to check box use $\boxtimes$

\end{enumerate}





% And we're done
\end{document}
