This must be a fun project. Just to throw a few ideas out there..
I've never done a theorem prover, but a while back, I was thinking about *where* a proof generated by such a program ought to get published. One idea was to publish the result on a purpose built *blockchain*.
Now given the current crypto market rout, "blockchain" is not the sexy word it once used to be, but pls hear me out..
CA proofs are often exhaustive calculations against a huge combinatorial search space. Now while the programs themselves are small, their outputs (the formal proofs) can run into tera or petabytes. So we might *not want* to record the actual output anywhere and instead record that output in its *compressed*, "Kolomogrov" form: i.e. the program itself.
The problem, of course, is that in order verify the result of the program (the prover), you'd have to run the program to completion. What if the prover takes days to finish (halt)? That wouldn't be ideal.
So the blockchain I'm fantasizing about, records both the prover program, and also various checkpoints (analogous to a program's state when suspended at a breakpoint in the debugger) along its execution path. That way, you'd be able to load the prover's state at say its trillionth operation. Kinda random access.
I was thinking the chain's currency (it's native token /unit of worth) could be made to correlate with the flop rate of the network (analogous to hash rate, hash power of a PoW chain). There'd be an on-chain bid and ask system to both offer new prover problems and for submitted solutions, together with an incentive system for any user to check/challenge claims that a program (prover) has been run to generate said checkpoints. Supposing the we call its currency/token *fuzz *, a fuzz would represent X units of flops on said network
I have developed this idea further in a Google doc, if anyone interested