Embracing AI and formalization: Experimenting with tomorrow’s mathematical tools

You have heard the buzz: AI and formalization will revolutionize mathematics. Computers will soon surpass humans in solving olympiad-style problems. Humans will transition from proving research-level theorems on their own to guiding computers. And maybe you even believe the hype. Other than pulling out your hair waiting for the day when computers take your job, what can you do? If you are like most career mathematicians, you are already overwhelmed with too many academic responsibilities, reserving any precious spare work hours for research. Where are you going to find the time to learn Lean or machine learning techniques? While I do not have the answers, I can share how I have embraced the potential of AI and formalization in mathematics through the <italic>eXperimental Lean Lab</italic> (XLL) at the University of Washington. I hope to inspire you to also get involved and play an active role in guiding the transformation of our field.