[YeGoblynQueenne]

>> 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.