People could send e-mail containing a conjecture in combinatory logic, the conjecture would be given to the theorem prover ITP, and the results of the search would be returned by e-mail, all without human intervention.
See ``A Note on Smullyan's Birds'', by Overbeek and Glickfeld, Association of Automated Reasoning Newsletter #7, October 1986.
These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.