Formalization of Anabelian Geometry (25rit037)

Organizers

Adam Topaz (University of Alberta)

Johan Commelin (Utrecht University)

Yuichiro Hoshi (Kyoto University)

Fumiharu Kato (ZEN university)

Description

The Banff International Research Station will host the "Formalization of Anabelian Geometry" workshop at UBCO Okanagan from May 25 - 31, 2025.


Formal mathematics is a rapidly emerging field within pure mathematics, where mathematical definitions, theorems and proofs are encoded into a formal language that can be verified and processed using a specialized piece of computer software called a proof assistant. One of the most popular modern proof assistants among mathematicians is called Lean4, whose mathematical foundations are much more algorithmic in nature when compared with the standard set-theoretic foundations of mathematics. From this perspective, the formalization of anabelian geometry is particularly intriguing, since this is a subject within pure mathematics (specifically, within arithmetic geometry) whose focus is on building algorithms which, roughly speaking, construct one kind of mathematical object from another.



The research team associated with this proposal will be digitizing certain constructions, definitions, theorems and proofs from anabelian geometry using the Lean4 proof assistant and its open-source mathematical library mathlib. They will focus primarily on the algorithmic aspects of such a formalization, while studying how the formalized anabelian algorithms themselves interact.


The Banff International Research Station for Mathematical Innovation and Discovery (BIRS) is a collaborative Canada-US-Mexico venture that provides an environment for creative interaction as well as the exchange of ideas, knowledge, and methods within the Mathematical Sciences, with related disciplines and with industry. The research station is located at The Banff Centre in Alberta and is supported by Canada's Natural Science and Engineering Research Council (NSERC), the U.S. National Science Foundation (NSF), and Alberta's Advanced Education and Technology.