A few impetuses:

• jacuzzi incident
• FrontierMath symposium
• DARPA expMath, Renaissance Philanthropy AI for Math Fund, ...

A few impetuses:

• Jacuzzi incident
• FrontierMath symposium
• DARPA expMath, Renaissance Philanthropy AI for Math Fund, ...
• Steadily growing discourse within mathematics community
  • "Some thoughts on automation and mathematical research"
  • Bulletin of the AMS vol 61 no.2 2024
  • "AI Will Become Mathematicians’ ‘Co-Pilot’"

  • Quanta series
  • various conferences and workshops (IAS, UCI, ...)
  • I'm sure much more

https://www.youtube.com/watch?v=eNgUQlpc1m0

• 2012: AlexNet wins ImageNet competition
• 2015(??): recurrent neural network trained on the Stacks project

• 2012: AlexNet wins ImageNet competition
• 2015(??): recurrent neural network trained on the Stacks project
• June 2016: transformer architecture introduced in by Vaswani et al (Google)
• November 2022: OpenAI releases ChatGPT (based on GPT-3.5)
• March 2023: GPT-4 released
• July 2024: DeepMind AI system solves four out of six IMO problems (silver medal?)
• September 2024: openAI releases o1 reasoning model
• November 2024: EpochAI introduces FrontierMath benchmark with contributions from over 60 mathematicians (including Fields medalists). Leading models score $<2\%$
• December 2024: o3 released, claims $25\%$ accurate on FrontierMath benchmark (some controversy)
• January 2025: DeepSeek released R1, supposedly competitive with o1 but much cheaper and open source

Formalization of mathematics?

• Lean and mathlib is rapidly growing in popularity
• 2021: Scholze's Liquid Tensor Experiment
• 2022: sphere eversion
• supposedly undergraduate mathematics in now entirely formalized

• Kevin Roose: one or more AI companies will claim AGI by 2026 or 2027
• AI2027: world ends by mid 2030

• Kevin Roose: one or more AI companies will claim AGI by 2026 or 2027
• AI2027: world ends by mid 2030
• Christian Szegedy (xAI, formerly worked on automating mathematics at Google): a computer system will match or exceed the problem-solving ability of the best human mathematicians by 2026
• Terry Tao (June 2024):

  "I think in three years AI will become useful for mathematicians. It will be a great co-pilot. You’re trying to prove a theorem, and there’s one step that you think is true, but you can’t quite see how it’s true. And you can say, “AI, can you do this stuff for me?” And it may say, “I think I can prove this.” I don’t think mathematics will become solved. If there was another major breakthrough in AI, it’s possible, but I would say that in three years you will see notable progress, and it will become more and more manageable to actually use AI. And even if AI can do the type of mathematics we do now, it means that we will just move to a to a higher type of mathematics. So right now, for example, we prove things one at a time. It’s like individual craftsmen making a wooden doll or something. You take one doll and you very carefully paint everything, and so forth, and then you take another one. The way we do mathematics hasn’t changed that much. But in every other type of discipline, we have mass production. And so with AI, we can start proving hundreds of theorems or thousands of theorems at a time. And human mathematicians will direct the AIs to do various things. So I think the way we do mathematics will change, but [Christian's] time frame is maybe a little bit aggressive."

• Objection #1: This is all just overblown hype.
• Rebuttal: There's a lot of hype, but see e.g. o3.
• Objection #2: Current AI systems are lousy at advanced mathematics, so we should be safe for a long time.
• Rebuttal: Look at progress over the last few years.
• Objection #3: There are bigger concerns for mathematicians right now (e.g. loss of NSF funding).
• Rebuttal: The policital pendulum always swings back and forth, but empirically technology moves only in one direction.
• Objection #4: If the above predictions are remotely true, so many aspects of society will change that it seems silly to worry about academic mathematics of all things.
• Rebuttal: Who else will be shepherd the fate of mathematics?
• Objection #5: There are already plenty of articles, conferences, etc about all of this.
• Rebuttal: Given the existential gravity of the situation, more seems reasonable.
• Objection #6: At any rate, there's not much we can do.
• Rebuttal: There are always way to influence the future. However, it is important to first get a better sense of what the future holds, and what are the possible outcomes, and which outcomes we wish to achieve.

• Should we start teaching Lean to our students (and ourselves)?
• Should mathematicians take control of their own AI benchmarks?
• Should we try to codify the goals and values of mathematical inquiry?
• Will it be necessary for mathematics to become more outward facing?
• What would we DO with a superhuman mathematical machine?