doc: fix typo in Validating a Lean Proof (#850)

Was "we use malicious to describe code _to go_ out of its way",
corrected to "we use malicious to describe code that _goes out_ of its
way" (emphasis highlights edit)

Author: OrfeasLitos

Manual/ValidatingProofs.lean

@@ -36,7 +36,7 @@ In particular, we use {deftech}_honest_ when the goal is to create a valid proof
 This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the {option}`debug.skipKernelTC`).
 Note that the {keyword}`unsafe` marker on API functions is unrelated to whether this API can be used in an dishonest way.
 
-In contrast, we use {deftech}_malicious_ to describe code to go out of its way to trick or mislead the user, exploit bugs or compromise the system.
+In contrast, we use {deftech}_malicious_ to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system.
 This includes un-reviewed AI-generated proofs and programs.
 
 Furthermore it is important to distinguish the question “does the theorem have a valid proof” from “what does the theorem statement mean”.