> Would knowledge in automated theorem proving (e.g. knowing how coq works) be somehow transferable to research in this field? Possibly. First, Coq is not an

> Would knowledge in automated theorem proving (e.g. knowing how coq works) be somehow transferable to research in this field? Possibly. First, Coq is not an automated theorem proving tool; it's an interactive theorem prover. If by automated theorem proving, you're thinking of a tool like Z3 or CVC4 which find models of statements in a decidable theory (which are pretty much always mathematically uninteresting), then...absolutely! SAT/SMT are at the core of constraint-based synthesis. Heck, CVC4 has a SyGuS mode that won the synthesis competition one year. If you're referring to actually searching for interesting theorems, as done by tools like Vampire and Otter, then probably not. Last month, I was discussing the matching algorithm used in the paper "egg: Fast and Flexible Equality Saturation" with a collaborator. It uses code trees, which I read about a few months earlier in the Handbook of Automated Reasoning. It stands out because I had pretty much never encountered a mention of any of that stuff in the preceding several years. I touch on this slightly in this blog post, about the benefits of learning Coq towards synthesis: http://www.pathsensitive.com/2021/03/why-programmers-shouldnt-learn-theory.html http://www.pathsensitive.com/2021/03/why-programmers-shouldn... . (And the benefits I mention are in understanding the type theory, not the innards.) > What are some existing open-source program synthesis libraries/frameworks where we can tinker around and maybe make something with it? https://github.com/microsoft/prose https://github.com/microsoft/prose Sketch: Download and manual from https://people.csail.mit.edu/asolar/ https://people.csail.mit.edu/asolar/ https://egraphs-good.github.io/ https://egraphs-good.github.io/ I searched for a few others, but they're either tools rather than frameworks, not directly synthesis, or I couldn't find a download. Though I may as well plug my own Cubix framework: http://cubix-framework.com/ http://cubix-framework.com/ > Thanks! I'm super curious about this field and it's somewhat related to what I'm working on so I'm pretty interested to learn more! Awesome! I hope to see great things coming from you.