The conjecture that AI-assisted mathematical research requires an adversarial theorem-proving process

An adversarial process is a process in which AI-generated mathematical arguments are checked by an independent formal mechanism, such as an interactive theorem prover. Interactive theorem provers include systems such as Lean, Isabelle, and Coq. Adversarial-process conjecture. The path to AI assisting research mathematicians is through an adversarial process, likely involving interactive theorem provers. This proposal addresses the difficulty of trusting mathematical arguments generated in natural language by requiring formal verification; the source presents it as a medium-term path rather than a settled result, and its resolution remains open.