text:
\section{Introduction}

\begin{figure*}[t]
\noindent
\begin{minipage}{0.50\textwidth}
\begin{center}
\large{Lean {\sf mathlib}}
\end{center}
\begin{flushleft}
    {\bf Formal theorem statement:}  \\
    \texttt{{\color{blue}theorem} {\color{orange}exists\_subgroup\_card\_pow\_prime}  \\
    \quad [fintype G] (p : $\mathbb{N}$) \{n : $\mathbb{N}$\} \\
    \quad [fact p.prime] (hdvd: p \^{} n | card G) : \\
    \quad $\exists$ K : subgroup G, fintype.card K = p\^{}n \\}
\end{flushleft}
\end{minipage}\vline\phantom{v}\hfill%
\begin{minipage}{0.50\textwidth}
\begin{flushleft}
\begin{center}
\large{{\sf ProofNet} dataset (ours)}
\end{center}
\vspace{5pt}

{\bf Formal theorem statement:} \\
\texttt{{\color{blue} theorem} {\color{orange}exercise\_4\_5\_14} \{G : {\color{blue}Type}*\} \\
\quad [group G] [fintype G] \\
\quad (hG : card G = {\color{ForestGreen}312}) : \\
\quad $\exists$ (p : $\mathbb{N}$) (P : sylow p G), P.normal} \\
\vspace{5pt}
{\bf Natural language theorem statement: } \\
Prove that a group of order 312 has a normal Sylow $p$-subgroup for some prime $p$ dividing its order. \\
\vspace{5pt}
\textbf{Natural language proof: }
\end{flushleft}
    \begin{proof}
    Since $|G|=351=3^{2}.13$, $G$ has $3$-Sylow subgroup of order $9$, as well as $13$-Sylow subgroup of order $13$. Now, we count the number of such subgroups. Let $n_{13}$ be the number of $13$-Sylow subgroup and $n_{3}$ be the number of  $3$-Sylow subgroups. Now $n_{13}=1+13k$ where $1+13k|9$. Thus the only possible choice for $k$ is $0$. Hence, there is a unique $13$-Sylow subgroup and because it is unique it is normal.
    \end{proof}
\end{minipage}

\caption{A sample theorem statement from mathlib, show on the left, and a sample theorem statement from \textsf{ProofNet}, shown on the right. Mathlib emphasizes including the most abstract and general formulations of mathematical results, whereas \textsf{ProofNet} predominantly tests the ability of models to apply those results to concrete problems.}
\label{fig:style}
\vspace{-10pt}
\end{figure*}

The creation of an automatic mathematician, that is, a system capable of autonomously posing conjectures and proving theorems, is a longstanding challenge in mathematics and artificial intelligence \citep{gelertner1959}. In recent years, neural generative language modelling has emerged as a promising approach to automating aspects of mathematics \citep{rabe2021}.

One approach to applying language models to mathematics has been to treat mathematical reasoning in natural language as a sequence learning task \citep{welleck2021, welleck2022, lewkowycz2022}. A key advantage of mathematical reasoning in natural language is the abundance of natural language mathematics data on the internet \citep{lewkowycz2022}.

An alternative approach is to use language models to guide formal proof-search in an interactive theorem prover (ITP) \citep{yang, polu2020, polu2022, jiang2022}. A salient advantage of this method is that the ITP acts as a verifier for the language model's reasoning, enabling the natural implementation of bootstrapping techniques such as expert iteration \citep{silver2017, polu2022}.

{\it Autoformalization}, the task of automatically formalizing mathematics, seeks to build a bridge between informal and formal mathematical reasoning \citep{wang2018, szegedy2020, wu2022}, with the potential of extracting a training signal from vast corpora of natural language mathematics data while still grounding a system's reasoning in formal logic. However, lack of parallel data between informal and formal mathematics means that autoformalization suffers from a lack of standard benchmarks to guide progress in the field.

To remedy this gap, we propose \textsf{ProofNet},\footnote{Full dataset are available at \url{https://huggingface.co/datasets/hoskinson-center/proofnet}. Code to replicate experiments available at \url{https://github.com/zhangir-azerbayev/ProofNet}} a benchmark consisting of parallel natural language and formal mathematics that can be used to evaluate autoformalization and theorem proving. The \textsf{ProofNet} benchmark consists of 371 parallel formal theorem statements, natural language theorem statements, and natural language proofs sourced from the exercises of popular undergraduate-level pure mathematics textbooks. Formal statements are expressed in the Lean 3 theorem prover \citep{MouraKADR15}, and depend on Lean's {\sf mathlib} \citep{mathlib}.

Language-model-based theorem provers and autoformalization systems have typically been evaluated on benchmarks consisting of competition and olympiad-style problems \citep{zheng22, wu2022}. While such problems require complex reasoning, their solutions only depend on a relatively small set of elementary facts about integers, real numbers, counting, and geometry. In contrast, modern research mathematics requires the mastery of a massive body of theory made up of thousands of definitions, lemmas, and theorems. The Lean 3 formalization of perfectoid spaces, an important definition in research-level arithmetic geometry, depends on over 3000 distinct theorems and definitions \citep{buzzard2020}. How to effectively reason over such a large repository of knowledge is an important unsolved problem in applying language models to mathematics \citep{irving2016, wu2022mem, tworkowski2022} .

\textsf{ProofNet} falls short of requiring mastery of all of modern mathematics, but poses the still ambitious goal of reasoning over the core of an undergraduate mathematics, including basic analysis, algebra, number theory, and topology. We hope that this benchmark will spur the development of language models that are able to reason effectively over large knowledge bases.

In order to obtain stronger baselines on {\sf ProofNet}, we train and open-source the {\sc proofGPT} language models at scales of 1.3 billion and 6.7 billion parameters. These models are trained on the {\sf proof-pile}, an 8 billion token dataset of mathematical text. To our knowledge, these are the only open-source language models fine-tuned for general mathematics.

We establish baselines for {\sf ProofNet} theorem autoformalization using in-context learning \citep{brown2020}. Moreover we introduce two novel theorem autoformalization methods that outperform our few-shot baselines. {\it Prompt retrieval} uses nearest-neighbor search against an embedding database to create a prompt consisting of the {\sf mathlib} declarations most relevant to a particular natural language theorem. {\it Distilled backtranslation} is a method inspired by work in unsupervised machine translation \citep{lample2017, han2021} that finetunes a language model for autoformalization at a large scale without the need for parallel data.

\section{The \textsf{ProofNet} Benchmark}

\paragraph{Dataset collection} Problems in the \textsf{ProofNet} benchmark are primarily drawn from exercises in popular undergraduate mathematics textbooks. For a complete list of sources, see \autoref{appendix:sources}.

Not all textbook exercises lend themselves naturally to formalization. In particular, we only consider for inclusion in \textsf{ProofNet} problems meeting the following criteria:
\begin{itemize}
    \item {\it Self-containment}. Problems should only depend on the results commonly taught in an undergraduate curriculum. In particular, this rules out problems that are split into multiple sequentially dependent parts, or those using nonstandard notations.
    \item {\it Naturality of formalization.} Not all kinds of mathematical problems can be naturally formalized, such as word problems, and such problems are excluded. We do not include exercises that require computing an unknown quantity. We do not include problems that depend on parts of Lean's mathlib that are relatively less mature, such as Euclidean geometry or combinatorics.
    \item {\it Low risk of train-test overlap.} Because language models are often pre-trained on large corpora mined from the internet that include {\sf mathlib}, we refrain from including statements that are in mathlib or are likely to be added to mathlib in the future. In practice, this means we avoid the abstract ``theory-building'' style of theorems that constitute mathlib, and instead choose problems that involve applying general results to specific cases. For more insight into the stylistic differences between mathlib and \textsf{ProofNet} problems, see \autoref{fig:style}.
\end{itemize}
Beyond the above criteria, problems were selected for broad coverage of the undergraduate curriculum and to range in difficulty from straightforward applications of the definitions to those requiring tremendous creativity. Problems statements are transcribed into \LaTeX{} and formalized by human annotators proficient in Lean. Natural language proofs are adapted from online solutions manuals, or in a few cases, written by the annotators.

\paragraph{Supported Tasks} As \textsf{ProofNet} includes parallel natural language statements,
natural language proofs, and formal statements, the dataset supports the evaluation of the following distinct tasks:
\begin{itemize}
    \item {\it Formal theorem proving}. Given a formal statement of a theorem, produce a formal proof.

    \item {\it Informal theorem proving}. Given an informal statement, produce an informal proof.
    \item {\it Autoformalization and informalization of statements}. Given an informal (formal) statement, produce a corresponding formal (informal) statement.

    \item {\it Autoformalization of proofs}. Given an informal theorem statement, its informal proof, and its formal statement, produce a formal proof.
\end{itemize}

\section{The {\sc proofGPT} models}
    \begin{table}[t]
        \centering
        \begin{tabular}{lcc}
            \toprule
            Source & Size (GB) & Tokens \\
            \midrule
            arXiv.math & 13.6 & 4.9B \\
            Stack Exchanges & 0.96 & 0.3B \\
            Formal math libraries & 0.14 & 59M\\
            ProofWiki + Wikipedia math articles & 0.02 & 6.6M \\
            Open source books & 0.015 & 6.5M \\
            MATH & 0.002 & 0.9M\\
            \bottomrule \\
        \end{tabular}
        \caption{Composition of the {\sf proof-pile}.}
        \label{tab:pretrain}
    \end{table}

    \begin{table}[t]
        \centering
        \begin{tabular}{lcc}
            \toprule
            Model & {\sf arXiv.math} perplexity & {\sf proof-pile} perplexity\\
            \midrule
            {\it 1B parameters:} & &\\
            \quad Pythia 1.4B & 3.82& 4.12  \\
            \quad proof-GPT 1.3B & 3.17& 3.47  \\
            \midrule
            {\it 6B parameters:} & &\\
            \quad Pythia 6.9B & 3.36 & 3.62  \\
            \quad proof-GPT 6.7B &3.12  &3.43\\
            \midrule
        \end{tabular}
        \caption{Comparison of model perplexities on the test set of the {\sf arXiv} subset of the {\sf proof-pile} and the entire {\sf proof-pile}. Documents were joined using two newline characters and perplexity was calculated with a stride equal to the model's context length, which is 2048 for all models shown.}
        \label{tab:gpt}
    \end{table}

Many approaches to quantitative reasoning with language models depend on pre-training or fine-tuning a model on large corpora of mathematical text, which significantly boosts downstream performance \citep{hendrycks2021, polu2020, lample2022, lewkowycz2022}. Motivated by these results, we train and open-source the {\sc proofGPT} models at sizes of 1.3 billion and 6.7 billion parameters \footnote{\url{https://huggingface.co/hoskinson-center/proofGPT-v0.1}\\\url{https://huggingface.co/hoskinson-center/proofGPT-v0.1-6.7B}}. The {\sc proofGPT} models are decoder-only causual language models initialized with Pythia weights \citep{pythia}\footnote{The {\sc proofGPT} models were not initialized from the open-sourced weights of the Pythia models, but from a development version of the suite with slightly different hyperparameters. This is the cause of the small parameter discrepancy between a {\sf proofGPT} and the similarly sized Pythia model. Performance of the development versions of Pythia and the open-source versions are near-identical.}, and then fine-tuned on the {\sf proof-pile}, a corpus of mathematical text whose composition is detailed in \autoref{tab:pretrain}. Fine-tuning was performed using the GPT-NeoX library \citep{gpt-neox}. For training hyperparameters, see \autoref{appendix:training}. In \autoref{tab:gpt}, we show that the {\sc proofGPT} models outperform Pythia base models and GPT-2 at standard mathematical reasoning tasks.

We regard the {\sc proofGPT} model suite as inferior to the Minerva models \citep{lewkowycz2022} due to the fact that the {\sc proofGPT} models are fine-tuned on an order of magnitude less mathematical text and span a smaller parameter range. However, we hope that the research community will benefit from {\sc proofGPT}'s open-source weights and dataset.

\section{Methodology and Experiments}
In this work, we evaluate the capabilities of pre-trained language models on autoformalizing and informalizing theorem statements.
Due to the engineering challenges of implementing neural theorem proving systems in Lean, we leave an investigation of formal theorem proving and proof autoformalization to future work.

\subsection{Autoformalization methods}
We employ in-context learning with large language models as a strong baseline for the autoformalization of theorem statements \citep{wu2022}. Moreover, we introduce two novel methods for boosting autoformalization performance above the few-shot baseline: {\it prompt retrieval} and {\it distilled backtranslation}.

\subsubsection{Few-shot autoformalization and informalization} In-context learning is a simple and powerful method for adapting language models to sequence-to-sequence tasks \citep{brown2020}.

For our in-context baselines, we perform inference using the OpenAI API's {\it Code-davinci-002} endpoint \citep{chen2021} and the proofGPT 1.3B and 6.7B models. Prompts are listed are given in \autoref{appendix:few-shot}.

Because there may be multiple ways to formalize the same statement in Lean and no general way to automatically verify whether two statements that are not definitionally equal have the same mathematical content, autoformalizations are evaluated for correctness by a human expert. Informalizations are also judged by a human expert.

\subsubsection{Prompt retrieval} A blessing and a curse of current language models is that few-shot learning performance is highly sensitive to the exact prompt that is used \citep{kojima2022}. In particular, it is plausible that greater few-shot learning performance can be achieved by retrieving the few-shot examples that are most relevant to a particular question.

We implement a {\it prompt retrieval} procedure for statement autoformalization as follows. Suppose we have a knowledge-base $\mathcal{K}$ of formal statements. First, we generate an autoformalization $\hat{y}$ of a statement $x$ using our standard in-context procedure. Then we produce dense vector representations of $\hat{y}$ and the formal statements in $\mathcal{K}$. We retrieve the $k$-nearest-neighbors of $\hat{y}$ in $\mathcal{K}$, and include them in the few-shot prompt. For the precise format of the prompt, see \autoref{appendix:few-shot}.

We opt to retrieve against $\hat{y}$ instead of against $x$ because this method was significantly more performant in our preliminary experiments.

In our experiments, we create a knowledge-base $\mathcal{K}$ by taking our $y$s to be 90,530 statements from Lean {\sf mathlib} and use $k=4$. We use the OpenAI API's {\it embedding-ada-002} endpoint to generate text embeddings.

\subsubsection{Distilled backtranslation} A significant obstacle to fine-tuning language models on the autoformalization of theorem statements is the lack of large parallel corpora of formal and informal mathematics. In the face of this limitation, we draw on prior work leveraging generative models for unsupervised translation between natural languages. In particular, we use {\it distilled backtranslation}, a methodology inspired by \cite{han2021}.

Distilled backtranslation proceeds as follows. Suppose we have a large language model $P_{LLM}(\cdot)$ pre-trained on monolingual data in both the source and target language, a monolingual corpus $\{Y_i\}$ in the target language. We wish to fine-tune a ``student'' model $P_\theta(Y|X)$ to translate a sequence $X$ in the source language to a corresponding sequence $Y$ in the target language. First, we manually construct a few-shot prompt $C$ consisting of $X|Y$ pairs. Then, we sample synthetic backtranslations $X_i \sim P_{LLM}( X | C, Y_i)$. Finally, we fine-tune $P_\theta(\cdot)$ on the synthetic pairs to predict $P(Y|X)$.

In our experiments, we fine-tune proofGPT-1.3B using distilled backtranslation with informal mathematics as the source language and Lean 3 theorems as the target language. We use the theorems in Lean's mathlib as the target language's monolingual corpus. We use {\it Davinci-codex-002} as our teacher LM and proofGPT-1.3B as our student model. Fine-tuning hyperparameters are described in \autoref{appendix:finetuning}

\section{Results and Discussion}
\begin{table}
  \centering

      \begin{tabular}{lcccccc}
      \toprule
              & \multicolumn{3}{c}{\it Formalization} & \multicolumn{3}{c}{\it Informalization}\\
              \cmidrule(r){2-4} \cmidrule(r){5-7}
        Model &  Typecheck rate& BLEU & Accuracy & Compile rate& BLEU & Accuracy\\
        \midrule
        {\it Few-shot.} & & & & & &\\
        proofGPT-1.3B &5.9 & 8.1 &0 &0.77 & 5.1&4.3\\
        proofGPT-6.7B  & 4.3 &4.7  &0  & 0.70  & 6.0 & 6.5 \\
        Codex    & 23.7  & 25.1  &13.4 & 100  & 13.2  & 62.3  \\
        \midrule
        {\it Prompt retrieval:} & & & & & & \\
        Codex & 45.2 & 14.8 & 16.1 & -&- &- \\
        \midrule
        {\it Dist. backtrans.} &&&&&\\
        proofGPT-1.3B & 19.4  & 10.7  & 3.2  & - & - & - \\
        \bottomrule\\
      \end{tabular}
    \caption{Results of few-shot learning with LLMs on formalization and informalization of \textsf{ProofNet} statements. In addition to reporting autoformalization accuracy, we also report {\it typecheck rate}, which is the proportion of a model's samples that are well-formed statements in Lean's dependent type theory. If a model simply copies a formal statement from its prompt, we do not consider that a positive sample when calculating typecheck rate. For the informalization task, we also report {\it compile rate}, i.e what proportion of the model's samples produce \LaTeX{} that compiles. The most common reason why informal generations fail to compile is that they contain Unicode characters frequently used in Lean's mathlib but not accepted by the pdflatex compiler. To calculate BLEU scores, we split on whitespace and use BLEU-4 with smoothing. Note that formalization BLEU scores being higher than informalization BLEU scores is likely because natural language contains more lexically distinct but semantically equivalent statements.}
    \label{tab:results}
\end{table}

\subsection{In-context learning}
In \autoref{tab:results}, we present our experimental results for autoformalization and informalization of \textsf{ProofNet} theorem statements. Although conceptually simple and easy to implement, our {\it Code-davinci-002} in-context learning baseline achieves highly nontrivial performance, correctly formalizing 13.4\% of theorems. The {\sc proofGPT} models do not formalize any statements correctly, likely owing to their smaller parameter count. However, they demonstrate some signal on the typecheck rate and BLEU metrics. Note that even generating statements that typecheck in Lean 3's strict type theory is a nontrivial feat.

Informalization accuracy is much higher than formalization accuracy for all models, supporting the intuitive claim that informalization is an easier task than formalization. This result also suggests that large pre-trained language models have a strong grasp of the semantics of formal mathematics, and primarily struggle with generating lexically correct and type correct Lean code.

We further observe that among {\it Code-davinci-002}'s generations that typecheck, roughly half are correct formalizations. This is consistent with our hypothesis that {\it Code-davinci-002} has a strong grasp of the semantics of mathematics, since the model displays high accuracy conditional on having generated valid Lean.

\subsection{Prompt Retrieval and Distilled Backtranslation}
In \autoref{tab:results}, we additionally include autoformalization scores for the prompt retrieval and distilled backtranslation models. Applying prompt retrieval to the \textit{Code-davinci-002}{} model significantly boosts performance, increasing accuracy by 2.7 points and, notably, increasing typecheck rate by 21.5 points.

Distilled backtranslation improves the autoformalization performance of the {\sc proofGPT} 1.3B model not merely above the in-context performance of {\sc proofGPT} 1.3b, but also above the in-context learning performance of {\sc proofGPT} 6.7B.

\paragraph{Automatic metrics} Typecheck rate correlates strongly with formalization accuracy, and we recommend that typecheck rate be used as a predictor of autoformalization performance when evaluating accuracy is too costly. The BLEU metric correlates well with performance on many NLP tasks \citep{bleu}, but correlates poorly with performance code tasks \citep{chen2021}. Our findings illustrate that just as with code, BLEU is a poor guide to formalization performance, as prompt retrieval increases \textit{Code-davinci-002}{} formalization accuracy but decreases BLEU by over 10 points.

\subsection{Qualitative Analysis}
We ground our remaining analysis in four case studies: two that demonstrate successful formalizations produced by \textit{Code-davinci-002}, and two that are representative of our methods' most common failure cases.

\paragraph{Case study 1.} The following is a correct and idiomatic Lean mathlib formalization of exercise 10.7.4 in Michael Artin's {\it Algebra} produced by \textit{Code-davinci-002}:
\begin{center}
\begin{tabular}{|l|}
\toprule
     NL: Let $R$ be a ring, with $M$ an ideal of $R$. Suppose that every element of $R$ which is not in\\ $M$ is a unit of $R$. Prove that $M$ is a maximal ideal and that moreover it is the only maximal\\ ideal  of $R$.
  \\
\midrule
    {\it Code-davinci-002} output: \\
     \texttt{{\color{blue}theorem} {\color{orange}exercise\_10\_7\_10} \{R : {\color{blue}Type}*\} [ring R] (M : ideal R)} \\
     \texttt{  (hM : $\forall$ x : R, x $\notin$ M $\to$ is\_unit x)} :\\
     \texttt{  is\_maximal M $\wedge$ $\forall$ (N : ideal R), is\_maximal N $\to$ N = M}\\
\bottomrule
\end{tabular}
\end{center}
In this example, \textit{Code-davinci-002}{} demonstrates strong knowledge of {\sf mathlib} and some reasoning capability. For example, the model correctly identifies that ideals are expressed using a typeclass \texttt{ideal R}, but maximal ideals are expressed using a predicate \texttt{is\_maximal}. Moreover, the model correctly recognizes that an instance of the \texttt{ideal} type can be implicitly coerced to a \texttt{set R} in order to apply the set-theoretic notation \texttt{$\notin$}. Finally, the model correctly infers that the best way to express ``only maximal ideal'' is the statement \texttt{$\forall$ (N : ideal R), is\_maximal N $\to$ N = M}, which demonstrates some logical reasoning ability.

\paragraph{Case study 2.} The following problem, exercise 6.4.2 from Michael Artin's {\it Algebra}, is an example of vanilla {\it Davinci-code-002} making a mistake that is rectified by prompt retrieval.
\begin{center}
\sethlcolor{pink}
\begin{tabular}{|l|}
\toprule
     NL: Prove that no group of order $pq$, where $p$ and $q$ are prime, is simple.
  \\
\midrule
    {\it Code-davinci-002} output: \\
     \texttt{{\color{blue}theorem} {\color{orange}exercise\_6\_4\_2} \{G : {\color{blue}Type*}\} [group G] [fintype G] \{p q : $\mathbb{N}$\}}\\
     \texttt{(hp : nat.prime p) (hq : nat.prime q) (h : fintype.card G = p * q) :}\\
     \texttt{$\neg$ \hl{simple\_group} G} \\
\midrule
    {\it Code-davinci-002} + retrieval output: \\
     \texttt{{\color{blue}theorem} {\color{orange}exercise\_6\_4\_2} \{G : {\color{blue}Type*}\} [group G] [fintype G] \{p q : $\mathbb{N}$\}}\\
     \texttt{[hp : fact(nat.prime p)] [hq : fact(nat.prime q)]} \\
     \texttt{(h : fintype.card G = p * q)} :\\
    \texttt{\sethlcolor{green}$\neg$ \hl{is\_simple\_group} G} \\
\bottomrule
\end{tabular}
\end{center}
Vanilla {\it Davinci-code-002} makes a single lexical error: the model has correctly formalized the hypotheses of the problem, but has tried to use a nonexistent predicate \texttt{simple\_group} instead of the correct \texttt{is\_simple\_group}. The retrieval-augmented model uses the correct declaration because one of the retrieved {\sf mathlib} statements explicitly uses \texttt{is\_simple\_group}.

\paragraph{Case study 3.} The following is an incorrect formalization of exercise 6.16 from Sheldon Axler's {\it Linear Algebra} produced by \textit{Code-davinci-002}. The retrieval-augmented \textit{Code-davinci-002}{} autoformalization, not shown here, is also incorrect.
\begin{center}
\sethlcolor{pink}
\begin{tabular}{|l|}
\toprule
     NL: Suppose $U$ is a subspace of $V$. Prove that $U^{\perp}=\{0\}$ if and only if $U=V$
  \\
\midrule
    {\it Code-davinci-002} output: \\
     \texttt{{\color{blue}theorem} {\color{orange}exercise\_6\_16} \{K : {\color{blue}Type}*\} [field K]} \\
     \texttt{  \{V : {\color{blue}Type}*\} [add\_comm\_group V] [\hl{vector\_space K V}] \{U : \hl{subspace V}\} :}\\
     \texttt{  U.\hl{orthogonal} = \hl{\{0\}} $\leftrightarrow$ U = $\top$}\\
\midrule
    {\it ProofNet} label: \\
    \texttt{{\color{blue}theorem} {\color{orange}exercise\_6\_16} \{K : {\color{blue}Type}*\} [is\_R\_or\_C K] [inner\_product\_space K V] }\\
     \texttt{  (U : submodule K V) :}\\
     \texttt{  U.orthogonal = $\bot \leftrightarrow$ U = $\top$}\\

\bottomrule
\end{tabular}
\end{center}
Here, \textit{Code-davinci-002}{} makes three straightforward lexical mistakes: in {\sf mathlib}, vector spaces over a field $K$ are denoted by \texttt{module K V} rather than \texttt{vector\_space K V}, subspaces of a vector space by \texttt{submodule K V} rather than \texttt{subspace V}, and the trivial subspace is denoted by \texttt{$\bot$} rather than \texttt{\{0\}}. However, the model also makes a much more significant logical error. In order for the orthogonal complement $U^\perp$ of a subspace to make sense, the space must be endowed with a {\it inner product space} structure rather than merely a vector space structure, which is expressed in {\sf mathlib} as \texttt{inner\_product\_space K V}. Furthermore, inner product spaces are only defined over the real and complex fields, so one must also declare \texttt{[is\_R\_or\_C K]}. Reliably inferring these kinds of implicit hypotheses is a major challenge for autoformalization systems.

\paragraph{Case Study 4: Looping.} When generating formal and natural language theorem statements with {\sc proofGPT}s, the model will often repeatedly generate the same short phrase instead of producing a plausible theorem. For example, consider the attempted formalization of exercise 10.1.13 from Michael Artin's {\it Algebra} generated by {\sc proofGPT} 6.7B via in-context learning.
\begin{center}
\begin{tabular}{|l|}
\toprule
     NL: An element $x$ of a ring $R$ is called nilpotent if some power of $x$ is zero.\\ Prove that if $x$ is nilpotent, then $1+x$ is a unit in $R$.
  \\
\midrule
    {\it proofGPT-6.7b} output: \\
\texttt{{\color{blue}theorem} nilpotent\_of\_nilpotent\_of\_nilpotent\_of\_nilpotent\_of\_nilpotent}\\
\texttt{nilpotent\_of\_nilpotent\_of\_nilpotent\_of\_nilpotent\_of\_nilpotent\_of$\dots$}\\
\bottomrule
\end{tabular}
\end{center}
Prior work on decoding methods has shown that the likelihood of a repeated phrase increases with each repetition, and that greedy decoding generates text with higher likelihood than natural text \citep{holtzman}. These two findings constitute a plausible explanation for repetitive looping if the correct autoformalization is assigned low likelihood by the model. We observe that repetitive looping does not occur with {\it Code-davinci-002}, suggesting that the problem may disappear with scale (although there are many other differences between our small-scale models and {\it Code-davinci-002}).

\section{Related Work}

\paragraph{Language modeling for theorem proving} Language models have found success in theorem proving both in the natural language setting \citep{lewkowycz2022, welleck2021}, and within many major ITPs such as Metamath \citep{polu2020}, Isabelle \citep{jiang2022}, and Lean \citep{han2021pact, polu2022}. Popular benchmarks for evaluating language model-based provers are \cite{hendrycks2021} and \cite{welleck2021} for natural language, and \cite{zheng22} for formal.

\paragraph{Autoformalization} Recent work in autoformalization with language models was sparked by \citet{wu2022}, which demonstrated that models can autoformalize Isabelle theorem statements via in-context learning. In \citet{dsp}, the authors demonstrate a method for autoformalizing proofs in Isabelle. However, their method depends on the availibility of a performant black-box automated theorem prover, which is not available for Lean at the time of writing.

\paragraph{Interactive Theorem Proving} Work in formal theorem proving and autoformalization depends on libraries of formalized mathematics. This work directly depends on Lean's {\sf mathlib}, but indirectly benefits from lessons learned from other proofs systems such as Coq \citep{BertotC04}, Mizar \citep{GrabowskiKN10}, and Isabelle \citep{NipkowPW02}.

\paragraph{Unsupervised Machine Translation} Because the amount of parallel formal and natural language text is negligible, autoformalization faces many of the same challenges as unsupervised machine translation \citep{lample2017, han2021, garcia}. Our distilled backtranslation method is inspired by the distilled and iterated backtranslation algorithm of \citet{han2021}. However, the authors of this work regard backtranslation as a temporary hack and foresee that in-context learning will be enough to elicit maximal performance from a sufficiently good language model, as is now the case for unsupervised translation \citep{garcia}.
\section{Conclusion}
We introduced \textsf{ProofNet}, a benchmarking consisting of parallel natural language theorem statements, natural language proofs, and formal theorem statements in Lean 3. We have shown that pre-trained large language models achieve non-trivial but far from consistent performance via in-context learning on the autoformalization of \textsf{ProofNet} statements. Moreover, we have proposed prompt retrieval and distilled backtranslation, two methods that improve autoformalization performance above baseline.

\section*{Acknowledgments}

The authors would like to thank the Hoskinson Center for Formal Mathematics at Carnegie Mellon University for its generous funding and for providing a stimulating work environment. We additionally thank EleutherAI for providing compute to train the {\sc proofGPT} models.
Piotrowski was supported also by the grant of National Science Center, Poland, no. 2018/29/N/ST6/02903, and by the Kosciuszko Fundation.

\bibliographystyle{plainnat}

redpajama_set_name: RedPajamaArXiv


text:
\subsection{Finding the angle parametrization}
In this section we give the parametrization of hyperbolic Heron triangles in terms of angles and area, and
prove Theorem~\ref{th:heron-angles} and Corollary~\ref{cor:heron-angles-rank1}.
Note that throughout this paper we only consider the case of non-degenerate bounded triangles
(i.e., with no vertex at infinity), so that its angles and area are always positive and its side lengths finite.

Let $\alpha, \beta, \gamma >0$ denote the angles of a hyperbolic triangle.
Assume they are rational (as defined in the introduction) i.e.,
that $e^{i\alpha}, e^{i\beta}, e^{i\gamma} \in \mathbb{Q}[i]$.
Since the area $A = \pi - \alpha - \beta - \gamma$ we get that $A$ is also rational: $e^{iA} \in \mathbb{Q}[i]$.

If we denote by $a$ (resp.\ $b,c$) the side length opposite $\alpha$ (resp.\ $\beta, \gamma$),
the hyperbolic law of cosines (for the angles) reads:
\begin{equation}
    \label{eq:law-cos-1}
 \sin(\beta) \sin(\gamma) \cosh(a) = \cos(\alpha) + \cos(\beta) \cos(\gamma)
\end{equation}
and similar formulas involving $\cosh(b), \cosh(c)$.
As the angles are rational, it follows that $\cosh(a), \cosh(b), \cosh(c) \in \mathbb{Q}$.
To get a hyperbolic Heron triangle, it thus only remains to find the condition that $\sinh$ of $a,b,c$ are also
rational.

The (inverse of) the hyperbolic law of sines gives
\[
  \frac{\sinh(a)}{\sin(\alpha)} =
  \frac{\sinh(b)}{\sin(\beta)} =
  \frac{\sinh(c)}{\sin(\gamma)}.
\]
Multiplying by $\sin(\alpha)\sin(\beta)\sin(\gamma)$ we get:
\[
  \sinh(a)\sin(\beta)\sin(\gamma) =
  \sinh(b)\sin(\alpha)\sin(\gamma) =
  \sinh(c)\sin(\alpha)\sin(\beta).
\]
Call this quantity $\Delta_1$.
Squaring \eqref{eq:law-cos-1} we get
\[
    \sin(\beta)^2 \sin(\gamma)^2 (\sinh(a)^2 + 1) = (\cos(\alpha) + \cos(\beta) \cos(\gamma))^2
\]
and thus:
\begin{equation}\label{eq:Heroncondition}
  \Delta_1^2 = (\cos(\alpha) + \cos(\beta) \cos(\gamma))^2 - \sin(\beta)^2 \sin(\gamma)^2 \in \mathbb{Q}.
\end{equation}
Using trigonometric identities, we can rewrite this as a symmetric expression in
$\alpha, \beta, \gamma$:
\[
    \begin{array}{rcl}
        2\Delta_1^2 &=&  \cos(-\alpha + \beta + \gamma) + \cos(\alpha - \beta + \gamma)
            + \cos(\alpha + \beta - \gamma) \\
                    && + \cos(\alpha + \beta + \gamma) +
                \cos(2 \alpha) + \cos(2 \beta) + \cos(2 \gamma) + 1,
    \end{array}
\]
and we have that $\Delta_1 \in \mathbb{Q}$ if and only if all three of $\sinh(a)$, $\sinh(b)$, and $\sinh(c)$ are
rational.
Substituting $\gamma = \pi - A - \alpha - \beta$ and expanding the cosines, we obtain
(writing $c_A = \cos(A), s_A = \sin(A)$, etc...):

\begin{equation}\label{eq:c_Aandfriends}
  \begin{array}{rcl}
      2 \Delta_1^2 &=&
  (c_A^2 - s_A^2)\big[(c_\alpha c_\beta - s_\alpha s_\beta)^2 -  (c_\alpha s_\beta + c_\beta s_\alpha)^2\big]
                \\ &&
  - 4 c_A s_A\big[c_\alpha s_\alpha (c_\beta^2 - s_\beta^2) + c_\beta s_\beta(c_\alpha^2 - s_\alpha^2)\big]
                \\ &&
  - c_A\big[(c_\alpha c_\beta - s_\alpha s_\beta)^2 -  (c_\alpha s_\beta + c_\beta s_\alpha)^2
      + 2c_\alpha^2 + 2c_\beta^2 - 1\big]
                 \\&& +
  4 s_A(c_\alpha s_\alpha c_\beta^2 + c_\beta s_\beta c_\alpha^2) + 2 c_\alpha^2 + 2 c_\beta^2 - 1.
    \end{array}
\end{equation}

We wish to express this in terms of \emph{rational} angles.
Setting
\[  \renewcommand{\arraystretch}{1.5}
    \arraycolsep=1.5em
    \begin{array}{lll}
        \cos(A) = \frac{1 - m^2}{1+m^2}, &
        \cos(\beta) = \frac{1-u^2}{1+u^2}, &
        \cos(\alpha) = \frac{1-t^2}{1+t^2},        \\
        \sin(A) = \frac{2m}{1+m^2}, &
        \sin(\beta) = \frac{2u}{1+u^2}, &
        \sin(\alpha) = \frac{2t}{1+t^2},
  \end{array}
\]
and $w = (m^2+1)(u^2 + 1)(t^2 + 1)\Delta_1$,  equation \eqref{eq:c_Aandfriends} rewrites as:
\begin{align} \label{eq:w-t-angles}
    w^2  = & 4 m  (mu^2 - m - 2u)  (mt^2  -2t - m) \big[(mu^2 - m - 2u)t^2
                 \\& + (-4mu - 2u^2 + 2)t - mu^2 + m + 2u\big]. \nonumber
\end{align}
Finally, setting $n = m(m^2 + 1) (2u - m(u^2-1))$ and applying the change of variables
{\small
\begin{align*}
    y =& -\frac{(2u - m (u^{2} -1) )}{4  t^{3}}
\big[2(2u - m (u^{2} -1) ) (m u - 1) (m + u) m^{2} 2(t^{2} - 3)
        \\& +2  (m^{2} u^{2} - m^{2} - 6  m u - 2  u^{2} + 2) (2u - m (u^{2} -1)) m^{2} t^{2} + 2  (2u - m (u^{2} -1))^{2} m^{3}
        \\&-  (m u - 1) (m + u) m t w + (2u - m (u^{2} -1)) m^{2} w\big]
\\
        x  = &\frac{(2u - m (u^{2} -1))}{4t^2} \big[-4   (m u - 1) (m + u) m t +2  (m^{2} u^{2} + m^{2} - 2  m u + 2)
        m t^{2}
        \\&+ 2  (2u - m (u^{2} -1)) m^{2} + m w\big],
    \end{align*}}
with inverse
{\small
\begin{align*}
    t  =& - \frac{m(2u - m(u^2-1))(x - (m+u)^2(m^2+1))}%
    {y + (m+u)(1 - mu)(x-n)} \\

     w=&  2 m (2u - m(u^2-1))(y + (m+u)(1-mu)(x-n))^{-2}\\
      & \times \big[x^3-3(m^2+1)(u+m)^2x^2 \\&+m(m^2+1)^2(2u - m(u^2-1))(m^2u^4+2u^4+2mu^3+2m^2u^2+4u^2+6mu+3m^2)x \\&-m^2(m^2+1)^3(u+m)^2(u^2+1)(2u - m(u^2-1))^2+
      2(m^2+1)^2u^2(u+m)(mu-1)y\big]\\
\end{align*}
}
we get the equation:
\begin{equation}\label{eq:angles}
    y^2 = x  \big(x - n\big)  \big(x - n (u^2 + 1)\big).
\end{equation}
Its discriminant is $2^4 u^4 (u^2 + 1)^2  n^6 = 2^4 u^4 m^6 (u^2 + 1)^2 (m^2 + 1)^6 (2u - m(u^2-1))^6$.

We are ready to complete the proof of Theorem~\ref{th:heron-angles}.
\begin{proof}[Proof of Theorem~\ref{th:heron-angles}]
    It just remains to exhibit the open condition (A), which encodes the fact that the parameters give rise to
    an actual hyperbolic triangle.
    Assume first that the inverse of the change of variables is defined; this happens everywhere but on the
    line $y + (m+u)(1 - mu)(x-n) =0$.
    We claim that the conditions on $m,u,t$, along with their meaning are given by the following table:
\begin{table}[ht]
  \begin{tabular}{c|c}
    Condition & Translation\\\hline
  $m > 0$ & area $ A >0$ \\
  $t > 0$ & $\alpha > 0$ \\
  $u > 0$ & $\beta> 0$ \\
  $(tm + tu + mu -1)(tmu - t - m - u) > 0$ & $\gamma > 0$ \\
  $mu < 1$ & $\alpha + \beta + \gamma < \pi$.
    \end{tabular}
    \caption{Conditions for Theorem \ref{th:heron-angles} \label{table:conditionsheronangles}}
\end{table}
The first three conditions follow trivially from the circle parametrization, and so does the fourth one if one writes
the formula for the rational angle corresponding to $\gamma$.
For the fifth one, assuming the four others, we know that $0 < A, \alpha, \beta, \gamma < \pi$, and we must
find a condition encoding $A + \alpha + \beta + \gamma = \pi$.
By construction, any solution to \eqref{eq:angles} gives rise to a set of parameters satisfying this last
equation \emph{modulo} $2\pi$; thus we have $A + \alpha + \beta + \gamma \in \{\pi, 3\pi\}$ and we wish to
eliminate the $3\pi$ case.
For such a set of parameters, the $3\pi$ case happens exactly when any two elements in
$A, \alpha, \beta, \gamma$ sum up to $>\pi$.
Hence we can just pick the condition $A + \beta < \pi$, which translates as $mu < 1$ if one writes the
formula for the rational angles.

Now if $m,u$ are given parameters with $m,u>0$ and $mu < 1$, the conditions from Table \ref{table:conditionsheronangles} can be simplified to the
following open condition on the variable $t$:
\begin{equation}\label{eq:cond-A}
  \tag{A}  0 < t < \frac{1 - mu}{m+u}.
\end{equation}
Using the above change of variables, we get an open condition in terms of $x,y$ encoding the desired properties.

It remains to treat the case of points where the expression for $t$ is not defined, i.e., points of the curve
\eqref{eq:angles} lying on the line $y + (m + u)(1 - mu)(x - n)=0$.
There are 3 such points: the torsion point $T = (n,0)$, the point
\[
P =\big((m^2+1)(m+u)^2,u^2(m^2+1)^2(m+u)(mu-1)\big)
\]
and the third point $-(P+T)$.
Looking back at points on \eqref{eq:w-t-angles} mapping to the line, we find only one: the point $(w,t)$ with
\[
    t = \frac{2m(m+u)(1-mu)(2u - m(u^2-1))}{m^4u^4 - m^4u^2 -4m^3u^3 +m^4 +4m^3u +6m^2u^2 + u^2}.
\]
Its image is the point $P$.
So whenever this point exists and fulfills the condition \eqref{eq:cond-A} we get a pre-image for $P$, and
otherwise we do not.
The condition \eqref{eq:cond-A} thus needs to be strengthened to exclude those points.
\end{proof}

\subsection{Rank computations} \label{sub:angles-rank}
In this section we compute the rank of the above curve (fixing one parameter $u$ or $m$) and prove
Corollary~\ref{cor:heron-angles-rank1}.
We will write $E_{m,u}$ for the curve given by \eqref{eq:angles}, and $E_m$ (resp.\ $E_u$) for the same curve
seen over $\mathbb{C}(u)$ (resp.\ $\mathbb{C}(m)$).

\begin{lemma}\label{lem:rank-computations}
    The ranks of the $K3$ surfaces $E_m(\mathbb{C}(u))$ and $E_u(\mathbb{C}(m))$ fulfill the inequalities:
    \[
     1 \leq \quad \rk(E_m(\mathbb{C}(u))),\rk(E_u(\mathbb{C}(m))) \quad \leq 2.
    \]
    Moreover, the point
    \[
    P(m,u) =\big((m^2+1)(m+u)^2,u^2(m^2+1)^2(m+u)(mu-1)\big)
    \]
    is a point of infinite order on $E_{m,u}$, and the torsion group is isomorphic to
$\mathbb{Z}/2\mathbb{Z}\times\mathbb{Z}/2\mathbb{Z}$, with the points of order two given by
$(0,0), (n,0),$ and $(n(u^2+1),0)$.
    \end{lemma}
\begin{proof}
    The lower bound follows from the fact that $P$ is on the curve $E_{m,u}$ and of infinite order,
    which is easily verified by inspection. Alternatively one can see that the height pairing of the
    Mordell--Weil group on $E_u$ (resp.\ on $E_m$) gives $h(P)=2$.

    For the upper bound, we apply Tate's algorithm \cite[IV.9]{Silverman}.
    For $E_u(\mathbb{C}(m))$ we see that the singularities $m = 0, \pm i, \frac{2u}{u^2-1}$ are all of type $I_0^*$
    in the Kodaira classification, and so the number of components of each singular fiber is 5.
    Now by the Shioda--Tate formula (see \cite[Corollary~1.5]{Shioda}, or alternatively
    \cite[Corollary~6.7)]{SS-book}) we have
    \[
        \rho(E_u)=\rk(E_u(\mathbb{C}(m))) + 2 + 4 \cdot(5-1) = \rk(E_u(\mathbb{C}(m)))+18
    \]
    where $\rho(E_u)$ is the Picard number of $E_u$.
    Since $E_u$ is a $K3$ surface, we have ${\rho(E_u) \leq 20}$, and thus
    $\rk(E_u(\mathbb{C}(m))) \leq 2$.

    For $E_m(\mathbb{C}(u))$, we use the same formula.
    The singularities at $u=0$ and $u=\infty$ are of type $I_4$, the ones at $u=\pm i$ of type $I_2$ and the
    ones at the roots of $m u^2 -2u -m$ of type $I_0^*$.
    Applying the Shioda--Tate formula again,
    \[
    \rho(E_m)=\rk(E_m(\mathbb{C}(u))+2+2\cdot (4-1)+2\cdot (2-1)+2\cdot(5-1)=\rk(E_m(\mathbb{C}(u))+18.
    \]
    Thus $\rk(E_m(\mathbb{C}(u))) \leq 2$ also in this case.

  Finally, it is immediate to see that $(0,0), (n,0),$ and $(n(u^2+1),0)$ are points of order~2. Recall that the Euler characteristic satisfies $\chi=2$ for $K3$ surfaces. We combine this with the bound on the rank and Table (4.5) in \cite{MirandaPersson} to conclude that $E_u$ (resp. $E_m$) has torsion isomorphic to $\mathbb{Z}/4\mathbb{Z}\times \mathbb{Z}/2\mathbb{Z}$ or $\mathbb{Z}/2\mathbb{Z}\times \mathbb{Z}/2\mathbb{Z}$. Then one can check directly that the points of order 2 cannot be written as twice a point in  $E_u(\mathbb{C}(m))$ (resp. in $E_m(\mathbb{C}(u))$).
\end{proof}

If we set $u=1$ in the case of $E_u$, the singularities are at $m = 0, \pm i, \infty$ and the previous Lemma still applies. In this particular case, we can identify a second point of infinite order given by
\[
Q(m)=\big(2m(m+1)^2,i4m^2(m^2-1)\big).
\]
One can prove that the height pairing of the Mordell--Weil group on $E_1$ gives $h(Q)=2$, and that $\langle P,Q\rangle=0$, showing that $P(m,1)$ and $Q(m)$ are independent, and that the rank of $E_1(\mathbb{C}(m))$ is exactly 2.

We move on to the proof of Corollary~\ref{cor:heron-angles-rank1}.
\begin{proof}[Proof of Corollary~\ref{cor:heron-angles-rank1}]
    We need to show that for each fixed $m,u >0$ with $mu < 1$, there are infinitely many rational points
    on the curve $E_{m,u}$ satisfying the open condition \eqref{eq:cond-A}.
    By a theorem of Poincaré and Hurwitz (see \cite[Satz~11, p.~78]{Skolem})
    the rational points $E_{m,u}(\mathbb{Q})$ of $E_{m,u}$ are dense in $E_{m,u}(\mathbb{R})$ provided $E_{m,u}(\mathbb{Q})$ is
    infinite and both connected components of $E_{m,u}(\mathbb{R})$ contain a rational point.
    Hence the corollary will follow by density, once these two conditions are proven.

    Now by Lemma~\ref{lem:rank-computations}, $E_{m,u}(\mathbb{Q})$ has positive rank, so it is
    infinite.
    And since the 3 non-trivial torsion points are given by
    \[
      \big(0,0\big), \quad \big(n,0\big), \quad \big(n(u^2 + 1),0\big)
    \]
   and are rational, we conclude that both components have rational points.
\end{proof}

\subsection{Finding the side lengths parametrization}
This section is devoted to the parametrization of hyperbolic Heron triangles using side lengths.
The arguments are quite similar to those of Section~\ref{sec:heron-angles}, but using the (dual) hyperbolic
law of cosines for the side lengths.

Let $a,b,c$ denote the side lengths of a (non-degenerate bounded) hyperbolic triangle, and assume that
$e^a, e^b, e^c$ are rational.
Let $\alpha$ (resp.\ $\beta, \gamma$) be the angles opposing the sides of length $a$ (resp.\ $b,c$).
By the law of cosines (for the side lengths)
\begin{equation}
    \label{eq:law-cos-2}
    \sinh(b) \sinh(c) \cos(\alpha) = \cosh(b)\cosh(c)- \cosh(a)
\end{equation}
and hence $\cos(\alpha)$ is rational (and thus also $\cos(\beta)$ and $\cos(\gamma)$ for similar reasons).

Multiplying the hyperbolic law of sines
\[
  \frac{\sin(\alpha)} {\sinh(a)}=
  \frac{\sin(\beta)}{\sinh(b)} =
  \frac{\sin(\gamma)}{\sinh(c)}
\]
by $\sinh(a)\sinh(b)\sinh(c)$, we get
\[
    \sin(\alpha) \sinh(b) \sinh(c) = \sin(\beta) \sinh(a) \sinh(c) = \sin(\gamma) \sinh(a) \sinh(b).
\]
Call this quantity $\Delta_2$.
We have that $\Delta_2$ is rational if and only if $\sin(\alpha), \sin(\beta), \sin(\gamma)$ are rational.

As in Section~\ref{sec:heron-angles}, we square \eqref{eq:law-cos-2} to get
\[
    \sinh(b)^2 \sinh(c)^2(1 - \sin(\alpha)^2) = ( \cosh(b)\cosh(c)- \cosh(a))^2.
\]
Hence
\[
    \Delta_2^2 = \sinh(b)^2 \sinh(c)^2 - (\cosh(b) \cosh(c)  - \cosh(a))^2 \in \mathbb{Q}.
\]
As a side note, observe that if $A$ denotes the area of the triangle, we have
\[
    \sin(A) = -\sin(\alpha) \sin(\beta) \sin(\gamma) + \sin(\alpha) c_\beta c_\gamma + \sin(\beta) c_\alpha c_\gamma + \sin(\gamma) c_\alpha c_\beta
\]
where $c_\alpha = \cos(\alpha)$, etc...
Since $\frac{\Delta_2}{\sin(\alpha)} \in \mathbb{Q}$, and similarly for $\beta, \gamma$, we conclude that $\sin(A) = r\Delta_2$  for some $r \in \mathbb{Q}$.
Thus a hyperbolic triangle with rational side lengths has rational area exactly when $\Delta_2 \in \mathbb{Q}$, i.e., when all its angles are rational.

Rewriting the equation for $\Delta_2^2$ in a symmetric way, we get:
\[
  \Delta_2^2 = 1 - \cosh(a)^2 - \cosh(b) ^2 - \cosh(c)^2 + 2 \cosh (a) \cosh (b) \cosh (c).
\]
Letting $u = e^a, v = e^b$ and $w = e^c$ (so that $u,v,w \in \mathbb{Q}$), this equation rewrites as:
\[
    4 u^2 v^2 w^2 \Delta_2^2 = (uv - w) (uw - v) (vw - u) (uvw -1).
\]
We introduce the following change of variables
\[
y=\frac{2u(v^2-1)(w^2-1)(v^2w^2-1)\Delta_2}{vw(u-vw)^2}, \quad x=\frac{(v^2-1)(w^2-1)(uvw-1)}{vw(vw-u)},\\
\]
with inverse
\begin{align*}
    \Delta_2 &=\frac{(v^2-1)(w^2-1)(v^2w^2-1)y}{2\big(x+(v^2-1)(w^2-1)\big)\big(v^2w^2x+(v^2-1)(w^2-1)\big)},\\
    u &=\frac{v^2w^2x+(v^2-1)(w^2-1)}{vw\big(x+(v^2-1)(w^2-1)\big)}.
\end{align*}

This leads to the desired equation:
\begin{equation}\label{eq:sides}
    y^2 = x\left(x-(v-v^{-1})^2\right) \left(x-(w-w^{-1})^2\right).
\end{equation}
Its discriminant is given by $2^4(v-v^{-1})^4(w-w^{-1})^4(v^{-1}w-vw^{-1})^2(vw-v^{-1}w^{-1})^2$.

We can now proceed towards the proof of Theorem~\ref{th:heron-sides}.
\begin{proof}[Proof of Theorem~\ref{th:heron-sides}]
    It suffices to exhibit the open condition (B) that ensures the parameters give rise to a hyperbolic triangle.
    First, all the side lengths must be positive, whence $u >1$, $v>1$ and $w >1$.
    Second, the three triangle inequalities must be satisfied, i.e., $u < vw, v < uw$ and $w < uv$.
    Assuming $v,w$ are fixed and $>1$, we get the condition:
    \begin{equation} \label{eq:cond-B} \tag{B}
        \max\left(\frac{v}{w}, \frac{w}{v}\right) < u < vw.
    \end{equation}
    Under this condition, the above change of variable is always defined (and so is its inverse since $x$ is
    necessarily positive).
    Thus the theorem is proven.
\end{proof}

\subsection{Rank Computations}%
\label{sub:sides-rank}
This section is similar to \ref{sub:angles-rank}.
Let $E_{v,w}$ denote the curve given by \eqref{eq:sides}, and let $E_v$ (resp.\ $E_w$) denote the same curve
seen over $\mathbb{C}(w)$ (resp.\ $\mathbb{C}(v)$)).
Our goal is to give bounds on the rank of $E_v$ and $E_w$; since the equation for $E_{v,w}$ is symmetric in $v$
and $w$, it is enough to consider the curve $E_v$.
\begin{lemma}\label{lem:rank-computations-sides}
    The rank of the $K3$ surface $E_v(\mathbb{C}(w))$ satisfies
    \[
     1 \leq \quad \rk(E_v(\mathbb{C}(w)))\quad \leq 2.
    \]
    Moreover, the point
    \[
      R(v,w) = \big(-vw(v-v^{-1})(w-w^{-1}),ivw(v-v^{-1})(w-w^{-1})(vw-v^{-1}w^{-1})\big)
    \]
    is a point of infinite order on $E_{v,w}$.

    In addition, the torsion group is isomorphic to $\mathbb{Z}/4\mathbb{Z}\times\mathbb{Z}/2\mathbb{Z}$, generated by
\[S_0(v,w)=\big((v-v^{-1})(w-w^{-1}),i(v-v^{-1})(w-w^{-1})(v^{-1}-w^{-1})(vw+1)\big)\]
and  \[S_1(v,w)=\big((v-v^{-1})^2, 0\big).\]

    \end{lemma}

\begin{proof}
The proof of this result is very similar to that of Lemma \ref{lem:rank-computations}. As before,
the lower bound for the rank follows from the fact that $R$ is on the curve and of infinite order,
    which is easily verified by inspection. More formally, one can see that the height pairing of the Mordell--Weil group on $E_v$  gives $h(R)=\frac{1}{2}$.

  We observe that $E_v$ has singularities at $w=0, \infty,\pm 1$ of type $I_4$ in the Kodaira classification, while the singularities at $w=\pm v, \pm v^{-1}$ are of type $I_2$. By the Shioda--Tate formula, we have
 \[ \rho(E_v)=\mathrm{rk}E_v(\mathbb{C}(w))+2+4\cdot(4-1)+4\cdot(2-1)=\mathrm{rk}E_v(\mathbb{C}(w))+18.\]
    Since $E_v$ is a $K3$ surface, we have ${\rho(E_v) \leq 20}$, and thus
    $\rk(E_v(\mathbb{C}(w))) \leq 2$.

One can directly check that  $S_0$ and $S_1$ generate a subgroup isomorphic to $\mathbb{Z}/4\mathbb{Z}\times\mathbb{Z}/2\mathbb{Z}$. Combining the information about the rank and the Euler characteristic with  Table (4.5) in \cite{MirandaPersson} we conclude that the torsion group is given exactly by  $\mathbb{Z}/4\mathbb{Z}\times \mathbb{Z}/2\mathbb{Z}$.
\end{proof}

Even if Lemmas \ref{lem:rank-computations} and \ref{lem:rank-computations-sides} are very similar from the point of view of the arithmetic of the involved $K3$ surfaces, they contain a fundamental difference for the geometric problem. In the case of  Lemma \ref{lem:rank-computations}, the point $P(m,u)$ is defined over $\mathbb{Q}(m,u)$ and generates a nontrivial solution to the question of the Heron hyperbolic triangle with given area and angle. In contrast, the point $R(v,w)$ of Lemma \ref{lem:rank-computations-sides} is certainly not defined over $\mathbb{Q}(v,w)$, and we speculate that there is no point of infinite order over $\mathbb{Q}(v,w)$. This results in the following: we do not know a priori whether there is a Heron hyperbolic triangle with given sides $v$ and $w$. This will depend on the choice of $v$ and $w$, much like the classical congruent number problem depends on the choice of the area.

\section*{} \label{sec:intro}
\input{intro}
\section{Hyperbolic heron triangles -- Angle parametrization} \label{sec:heron-angles}
\input{heron-angles}

\section{Hyperbolic heron triangles -- Side length parametrization}\label{sec:heron-sides}
\input{heron-sides}

\section{Equilateral Triangles} \label{sec:equilateral}
\input{equilateral}

\section{Rational medians} \label{sec:medians}
\input{medians}

\section{Area bisectors} \label{sec:area-bisectors}
\input{area-bisectors}

\nocite{*}
\bibliographystyle{abbrv}