Centre for Mathematical AI
The integration of mathematics and artificial intelligence opens new avenues for accelerating research and discovery. The Fields Institute Centre for Mathematical AI serves as a collaborative platform where AI and mathematical expertise converge. Our mission is twofold: to develop tools that mathematicians can use without requiring extensive AI training, and to deepen our theoretical understanding of AI by applying mathematical rigour and insight.
As AI integrates fully into human lives, advanced mathematics is the best avenue to decode the “black box” decision-making processes behind today’s algorithms and to help build a roadmap that provides greater insight and direction when shaping these technologies.
Fields, with its long history of interdisciplinary collaboration and research excellence, has partnered with leading-edge AI research institutes to further strengthen capacity to drive innovation at the intersection of mathematics and AI.
The Centre’s work will focus on four research themes, including:
- Semi-automated generation of a dynamic knowledge tree from mathematical papers and mathematicians
- AI-assisted mathematical reasoning tools for mathematicians
- Automated formalization of mathematical papers
- Mathematical study and advancement of AI
Postdoctoral Fellowships
Applications are invited for two-year Fields Postdoctoral Fellowship positions with the research program on Mathematics for AI Safety, a joint initiative of the Fields Institute for Research in Mathematical Sciences and the Principles of Intelligence (PrincInt: https://princint.ai/), housed within the Fields Institute's Centre for Mathematical AI.The fellowships support research at the intersection of mathematics and AI safety, with a focus on developing rigorous mathematical foundations for AI interpretability. Research directions include mean field theories of deep learning, data attribution methods, renormalization group approaches to neural networks, learning-theoretic analysis of algorithms and geometric analysis of the learning landscape. Candidates are encouraged to interpret these subject areas broadly.Fellows will have access to mentorship from experts in relevant mathematical areas as well as AI safety researchers affiliated with PrincInt, the Schwartz Reisman Institute for Technology and Society, and the Vector Institute for Artificial Intelligence.Eligibility: Qualified candidates with a PhD in mathematics, statistics, physics, computer science or neuroscience are encouraged to apply. Women and underrepresented minorities are especially encouraged to apply. Fellowship positions are conditional on funding for the program.First-round selections will start in February 2026, and the posting will remain open until all positions are filled. The salary range for these fellowships is CAD$70,000 - CAD$90,000 per annum.
The Fields Institute is a centre for mathematical research activity - a place where mathematicians from Canada and abroad, from academia, business, industry and financial institutions, can come together to carry out research and formulate problems of mutual interest. Our mission is to provide a supportive and stimulating environment for mathematics innovation and education. Learn more about us.
Seminars
-
July 1, 2025 to June 30, 2026
Projects
Formalizing the Model Theory of Valued Fields
In recent years, formal proof verification has become an important mathematical topic in its own right. Modern interactive theorem provers such as Lean 4 provide powerful automation tools that bring us closer to a new reality where new mathematical discoveries also come with a formal certificate of soundness. However, to make this into a reality, more foundational results need to be formalized.
Large steps have already been taken by Lean's Mathlib library, containing essentially all of undergraduate mathematics. Yet, for most fields of mathematics, there is still a significant gap between what exists in the library and research-level mathematics.
We are leading an effort to bridge this gap for the model theory of valued fields. In particular, we will formalize relative quantifier elimination and the Ax-Kochen/Ersov principles. These are important tools in current research, underpinning e.g. frameworks for motivic integration, but they also have immediate consequences of interest to algebraic geometers and number theorists. While working towards this concrete goal, many supporting results with wide applicability will be developed, including quantifier elimination tests, and more fundamentally an extension of Lean's model theory library to the many-sorted setting.
You can check in on our progress at
https://github.com/Mathias-Stout/Many-sorted-model-theory
This repository is maintained by Aaron Crighton, John Nicholson and Mathias Stout.
----
Points of contact:
Deirdre Haskell
Aaron Crighton
Greg Cousins
John Nicholson
Mathias Stout
