María Inés Frutos Fernández and Michael B. Rothgang (Uni Bonn)
14:00 Michael Rothgang (Uni Bonn): Formalising differential geometry in Lean.
15:00 Tea and Coffee Break
15:30 María Inés de Frutos Fernández (Uni Bonn): Number Theory in the Lean Theorem Prover.
Michael Rothgang (Uni Bonn): Formalising differential geometry in Lean.
Abstract: Digitising or formalising mathematics refers to translating mathematical arguments from natural language (e.g. English) into a computer-readable format: this makes it possible to verify proofs with certainty, often improves mathematical understanding, can transform peer-review and enables new levels of collaboration. In recent years, there has been spectacular progress in formalising research-level mathematics in diverse fields. I will explain what the excitement is about and give an idea of the current state of the art.
In the second part, I will focus on differential geometry. Already finding the correct general definition is a non-trivial mathematical question. I will survey what is currently formalised, what is being worked on and where you can help. I will also comment on the technical challenges of working with manifolds in Lean and how to address them.
María Inés de Frutos Fernández (Uni Bonn): Number Theory in the Lean Theorem Prover.
Abstract: The Langlands program is a family of conjectures, mostly still open, that seek to establish deep connections between number theory, geometry, analysis, and representation theory. Stating these conjectures in Lean might lead to new insights into this theory; however, we are currently missing much of the background to do so.
In this talk I will discuss some of my work towards formalizing this background, including progress towards class field theory, Fontaine's period rings, and Drinfeld modules..
Wenn Sie digital an den Vorträgen teilnehmen möchten, wenden Sie sich bitte an Christian Molle molle @ uni-potsdam.de, um die Zugangsdaten zu erhalten.
