>> I do find the results interesting and wonder how well this translates into program synthesis for example. In broad terms it's the same generate-and-test app

>> I do find the results interesting and wonder how well this translates into program synthesis for example. In broad terms it's the same generate-and-test approach used for their AlphaCode system but with a theorem prover as a test step. In AlphaCode they use clustering and various heuristics to select programs, here they use the prover. Eventually, I expect, they'll figure out you can use an automated theorem prover to check the correctness of (logic) programs.