Abstract: 

Mathematics is on the brink of exciting and disruptive change. Recent developments in automatic formalisation (transforming human-readable proofs into machine-checkable proofs) open the door to rapid mathematical verification and exploration. How does this impact our work? Through examples of my own and others, I will discuss capabilities of current AI/formalisation tools (tools that *you* can use, "off the shelf", right now) in the context of mathematical research, and the challenges and opportunities this presents. This talk will be offline only.