diff --git a/ITP/conclusions.tex b/ITP/conclusions.tex
index ca5123c..f1fbef6 100644
--- a/ITP/conclusions.tex
+++ b/ITP/conclusions.tex
@@ -35,7 +35,7 @@
 that did not match the (correct) code of Heule and Scheucher.
 Our formalization corrects this.
 
-\subsection*{Future Work}
+\subparagraph*{Future Work}
 We hope to formally verify the result $h(7) = \infty$ due to Horton~\cite{hortonSetsNoEmpty1983},
 and other results in Erd\H{o}s-Szekeres style problems.
 
diff --git a/ITP/encoding.tex b/ITP/encoding.tex
index df25392..44121c5 100644
--- a/ITP/encoding.tex
+++ b/ITP/encoding.tex
@@ -154,7 +154,7 @@
 are both empty shapes in $P$,
 then $S$ is an empty shape in $P$.
 
-\subsection*{Running the CNF.}
+\subsection{Running the CNF.}
 \label{sec:running_cnf}
 Having now shown that our main result follows if $\phi_{30}$ is unsatisfiable,
 we run a distributed computation to check its unsatisfiability.
diff --git a/ITP/triple-orientations.tex b/ITP/triple-orientations.tex
index 3d851f7..a000063 100644
--- a/ITP/triple-orientations.tex
+++ b/ITP/triple-orientations.tex
@@ -222,7 +222,7 @@
 $\left(\mathbb{R}^2\right)^n$.
 This is the key idea that will allow us to transition from the finitely-verifiable statement ``\emph{no set of triple orientations over $n$ points satisfies property $\pi_k$}'' to the desired statement ``\emph{no set of $n$ points satisfies property $\pi_k$}.''
 
-\subsection*{Properties of orientations}\label{sec:sigma-props}
+\subsection{Properties of orientations}\label{sec:sigma-props}
 
 We now prove,
 assuming points are sorted left-to-right (which is justified in~\Cref{sec:symmetry-breaking}),