The talk will describe several ways in which machine learning is combined with theorem proving today over large corpora of formal proof. If time permits, I will also show some demos of the systems and mention related topics such as ML-guided conjecturing and autoformalization.