> It seems like the person you're responding to has decided a type checker... should be considered a scoring function
To clarify, I didn't decide this, this is a valid scoring function in AlphaEvolve. The scoring function is generic and can even be an LLM writing prose giving feedback on the solution followed by another LLM scoring that prose numerically. There needs to be a numeric score to rank solutions. Typically type checkers give more output than 1 or 0, though. For example, they'll often give you information about where the first error occurred.
That doesn't mean it's a great scoring function or even a good one. But it is a scoring function and without any scoring function at all progress would be impossible. To the extent that math is about writing proofs, it's a valid and essential scoring function for any problem. In practice, to make progress you need more than just the ability to write a logical proof, you need to build on previous results, add extra conditions, compute examples, etc. But in the context of the discussion, the point is that there is always some way to measure progress, which is why AlphaEvolve includes this mechanism.
> 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.
This is true, but it's also true that typically mathematicians fix a logic or universe before getting down to work. So AlphaEvolve and human mathematicians are on equal footing in that respect.