\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}

\newtheorem{theorem}{Theorem}

\title{Mysterious Proof: Main Theorem}
\author{Lean Proof Extraction}
\date{}

\begin{document}

\maketitle

\section*{Theorem Statement}

The following theorem is derived from the Lean definition \texttt{main\_theorem}.

\begin{theorem}
There exists a sequence of integers $(b_n)_{n=1}^{\infty}$ such that for all $n$, $b_n \in \{1, 2, 3, 4, 5\}$, and there exists a rational number $q \in \mathbb{Q}$ satisfying:
\[
\sum_{n=1}^{\infty} \frac{1}{2^n + b_n} = q
\]
\end{theorem}

\end{document}