diff --git a/ITP/conclusions.tex b/ITP/conclusions.tex index 262df19..ca5123c 100644 --- a/ITP/conclusions.tex +++ b/ITP/conclusions.tex @@ -39,10 +39,9 @@ \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. -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 -when the proof certificate is hundreds of terabytes, -as in this result (see \Cref{sec:running_cnf}). +We also want to improve the trust story of importing ``cube and conquer''-style results into an ITP. +Importing these kinds of proofs is a significant engineering task +when the proof certificate is hundreds of terabytes in size, +as it was for 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. +more work needs to be done to strengthen the trust in this connection point.