Formalization of Anabelian Geometry (25rit037)

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.