Search Clay Mathematics Institute

  • About
    About
    • About
    • History
    • Principal Activities
    • Who’s Who
    • CMI Logo
    • Policies
  • Programs & Awards
    Programs & Awards
    • Programs & Awards
    • Funded programs
    • Fellowship Nominations
    • Clay Research Award
    • Dissemination Award
  • People
  • The Millennium Prize Problems
    The Millennium Prize Problems
    • The Millennium Prize Problems
    • Birch and Swinnerton-Dyer Conjecture
    • Hodge Conjecture
    • Navier-Stokes Equation
    • P vs NP
    • Poincaré Conjecture
    • Riemann Hypothesis
    • Yang-Mills & the Mass Gap
    • Rules for the Millennium Prize Problems
  • Online resources
    Online resources
    • Online resources
    • Books
    • Video Library
    • Lecture notes
    • Collections
      Collections
      • Collections
      • Euclid’s Elements
      • Ada Lovelace’s Mathematical Papers
      • Collected Works of James G. Arthur
      • Klein Protokolle
      • Notes of the talks at the I.M.Gelfand Seminar
      • Quillen Notebooks
      • Riemann’s 1859 Manuscript
  • Events
  • News

Home — Events — Formalizing Class Field Theory

Formalizing Class Field Theory

Date: 21 - 25 July 2025

Location: Mathematical Institute, University of Oxford

Event type: CMI HIMR Summer School

Organisers: Kevin Buzzard (Imperial), Richard Hill (UCL)

Class Field Theory in its cohomological form is one of the highlights of early 20th century mathematics, and is now understood as the abelian case of the Langlands Philosophy. Although it sounds like science fiction to many mathematicians, some computer scientists are arguing that AI methods are progressing so fast that soon computers will be helping humans to push back the boundaries of research in the Langlands Philosophy. However, there is currently no concrete evidence that this is happening. Furthermore, using a language model alone to do mathematics at this level is problematic, because language models are error-prone, and one error in a mathematical argument invalidates it.

This summer school does not have anything to do with AI, but it has a lot to do with class field theory. During the school, we will be teaching class field theory to the Lean theorem prover. You can imagine the school as a group of people collaborating on writing a Bourbaki-like document explaining class field theory. Or you can imagine it as a group of people turning class field theory into a bunch of levels of a puzzle game and then solving these levels. Or you can imagine it as a group of people creating training data for a theorem prover-backed AI which can then try and learn some of these interesting mathematical ideas.

Prerequisites: Students should have some knowledge of Lean and a basic knowledge of cohomology groups, Cyclotomic fields, Kummer extensions and local fields. It is recommended that students work through some of the free online textbook Mathematics in Lean prior to the summer school. 

This event will be taking place in-person. Accommodation, lunch and subsistence will be provided; participants are expected to fund their own travel (limited funds may be available for those unable to secure travel costs from their home institution).

Registration: Please register your interest by completing the application form; your c.v. and a short supporting letter from your PhD supervisor will be required with your application. Closing date for registration is 1 May 2025. Successful applicants will be notified by 26 May 2025.  Student places are offered with accommodation. Registration is now closed.

With questions regarding the scientific program, please contact Kevin Buzzard.  With all other questions, please contact admin@claymath.org.

This summer school is jointly funded by the Clay Mathematics Institute, the Heilbronn Institute for Mathematical Research and the Mathematical Institute at the University of Oxford.

Share
A CMI event

Related events

See all events
See all events
  • Privacy Policy
  • Contact CMI

© 2025 Clay Mathematics Institute

Site by One