I will talk about new technologies for mathematical reasoning, including proof assistants, symbolic reasoning systems, and machine learning. These can be grouped under the broad heading “AI for mathematics,” but they are actually a collection of related technologies with interesting interactions between them. I will describe some notable achievements to date, and I will demonstrate the use of Lean, a proof assistant that has been gaining traction in the mathematics community.