Program synthesis is also pretty much equivalent to generating proofs of propositions by the Curry-Howard Isomorphism. There was a post from a few days ago about using ML to generate proofs in Lean. I'm sure there's ongoing research to do the same thing with synthesis (which imo is probably going to be more effective at pruning the search space than brute force).
