Rephrase ending paragraph

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.