I am interested in the formalization of mathematics using proof assistants, to make sophisticated arguments in number theory and arithmetic geometry more robust and reusable. Relatedly, I am drawn to carefully designed machine-learning methods for discovery and pattern-finding in large arithmetic datasets.