Interactive Theorem Provers
Most of times the pattern of proving and verifying it is like this $prove \to verify$, that is: there is an entity that generates the solution, andPo then another that tries to verify it. But more expressive algorithms could be possible if there is interaction between the two entities, ones that try to prove it, and others try to verify it. From some point of view, this is similar from what AlphaGo does when searching, there is a part that guides the search, another that actually searches for it. Or the modern alpha geometry in modern times. ...