Some adventures in learning synthesis of mathematical objects and proofs

I will talk about our adventures in designing feedback loops for learning-based synthesis of explanations for integer sequences in the OEIS (DOI 10.48550/arXiv.2301.11479), learning-based synthesis of instantiation proofs (DOI 10.48550/arXiv.2210.03590), and our recent advances in learning-based proof search.