future work discussion

ITP/conclusions.tex

@@ -35,12 +35,14 @@
 that did not match the (correct) code of Heule and Scheucher.
 Our formalization corrects this.
 
-In terms of future work,
-we hope to formally verify the result $h(7) = \infty$ due to Horton~\cite{hortonSetsNoEmpty1983},
+\subsection*{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.
-A key challenge for the community
-is to improve the connection between verified SAT tools and ITPs.
+
+We also see a key challenge for the community,
+to improve trust when importing ``cube and conquer'' style results to an ITP.
 This presents a significant engineering task
-for proofs that are hundreds of terabytes long (as in this result).
+when the proof certificate is hundreds of terabytes,
+as in this result (see \Cref{sec:running_cnf}).
 Although we are confident that our results are correct,
 the trust story at this connection point has room for improvement.

ITP/encoding.tex

@@ -154,7 +154,8 @@
 are both empty shapes in $P$,
 then $S$ is an empty shape in $P$.
 
-\subparagraph*{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.
 We solve the SAT formula~$\phi_{30}$ produced by Lean using the same setup as

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}),