Multiple tickets/tasks will fall under this initiative.
First, we must agree upon success criteria for running all proofs: how much time given to each theorem before timeout, specs of machine on which we are establishing our baseline, current metrics, target metrics, and due date
We should also improve accessibility by enabling large proof bases on lighter weight machines, possibly by requesting (and verifying e.g., by a signature) a set of previously-proved theorems remotely, importing them as lemmas during runtime.
We should also analyze K's searching algorithms & heuristics to identify opportunities for optimizations. A more "modular" proof mode may be beneficial here, so that they can be discharged to multiple processes or nodes.
Some improvements may be automatically gained by virtue of migrating to the Haskell backend. We should identify how this migration will affect performance as well
Multiple tickets/tasks will fall under this initiative.