Comment by measurablefunc

It seems like the person you're responding to has decided a type checker that outputs 1 when the proof object is valid according to the rules & 0 otherwise should be considered a scoring function. The objective function in this case is not differentiable so the usual techniques from deep learning will not work & genetic search algorithms like AlphaEvolve can in theory be used in these cases. Someone still has to come up w/ the type system & verify the soundness of the rules b/c there is no finite codification of all valid & sound type systems like there are for problems in the linked blog post.