I would like to give several examples and demos of feedback loops between reasoning, learning and conjecturing in mathematics and formal proof.  In the recent years such combinations are increasingly used for building stronger automated theorem provers, SMT solvers, better automation in interactive theorem provers, and for conjecturing in mathematics.  The methods in this field include equipping the current deductive systems with efficient statistically learned guidance that controls the choice of the inference steps, using for example neural networks, fast decision trees, and their combinations.  I will also discuss methods that try to directly synthesize reasoning objects such as instantiations and OEIS explanations, using various learning-based approaches.