BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:María Inés de Frutos-Fernández (Imperial College London)
DTSTART;VALUE=DATE-TIME:20220113T160000Z
DTEND;VALUE=DATE-TIME:20220113T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/1
DESCRIPTION:Title: Adeles and ideles\nby María Inés de Frutos-Fernández (Im
perial College London) as part of London Learning Lean\n\nLecture held in
Huxley 410.\n\nAbstract\nThe ring of adèles of a global field and its gro
up of units\, the idèles\, are fundamental objects in modern number theor
y. We will discuss a formalization of their definitions\, starting with so
me background on Dedekind domains and valuations\, and of some application
s\, including the statement of the main theorem of global class field theo
ry.\n\nThis seminar will be hybrid\; you can watch in person or on Zoom.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chris Birkbeck (University College London)
DTSTART;VALUE=DATE-TIME:20220120T160000Z
DTEND;VALUE=DATE-TIME:20220120T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/2
DESCRIPTION:Title: Modular forms and Eisenstein series\nby Chris Birkbeck (Un
iversity College London) as part of London Learning Lean\n\n\nAbstract\nI
’ll discuss some recent work on defining modular forms and Eisenstein se
ries in LEAN. Modular forms are some of the most important objects in numb
er theory due in part to their role in the proof of Fermat’s Last Theore
m. These special functions act as glue between algebra\, geometry and ana
lysis\, it is therefore tempting to begin formalizing them. Moreover one w
ants to formalise interesting examples\, such as Eisenstein series. In the
talk I will discuss the mathematics behind there definitions and highligh
t the main challenges in formalising them.\n\nThis talk will be a Zoom tal
k. I (Kevin Buzzard) am not in London this week so I will not be running t
he show in the usual room\, and do not know if anyone will be there to run
it because I was too disorganised to sort anything out before I left Lond
on. See you on Zoom!\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Amelia Livingston (London School of Geometry and Number Theory)
DTSTART;VALUE=DATE-TIME:20220127T160000Z
DTEND;VALUE=DATE-TIME:20220127T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/3
DESCRIPTION:Title: Group cohomology\nby Amelia Livingston (London School of Ge
ometry and Number Theory) as part of London Learning Lean\n\n\nAbstract\nW
e can study a group $G$ by applying homological algebra to modules $M$ ove
r the group ring $\\mathbb{Z}[G]$\, via calculating the groups $\\mathrm{E
xt}_{\\mathbb{Z}[G]}^n(\\mathbb{Z}\, M)$. However\, these groups are bless
ed with a nice concrete description in terms of the set of functions $G^n
\\to M$. I've been using mathlib's relatively new homological algebra libr
ary to marry the concrete description to the more abstract formulation giv
en by Ext. I will talk about the quirks of homological algebra in Lean\, t
he challenges I faced\, and plans to extend this work to Galois cohomology
.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alena Gusakov (University of Waterloo)
DTSTART;VALUE=DATE-TIME:20220303T160000Z
DTEND;VALUE=DATE-TIME:20220303T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/4
DESCRIPTION:Title: Introduction to matroids\nby Alena Gusakov (University of W
aterloo) as part of London Learning Lean\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ashvni Narayanan (Imperial College London)
DTSTART;VALUE=DATE-TIME:20220310T160000Z
DTEND;VALUE=DATE-TIME:20220310T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/5
DESCRIPTION:Title: p-adic L-functions\nby Ashvni Narayanan (Imperial College L
ondon) as part of London Learning Lean\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Oliver Nash (Imperial College London)
DTSTART;VALUE=DATE-TIME:20220317T160000Z
DTEND;VALUE=DATE-TIME:20220317T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/6
DESCRIPTION:Title: Engel's theorem in Mathlib\nby Oliver Nash (Imperial Colleg
e London) as part of London Learning Lean\n\n\nAbstract\nI will discuss th
e formalisation of Engel's theorem for nilpotent Lie algebras in Lean's Ma
thlib library.\n\nI will emphasise how Mathlib's strategy of making very g
eneral definitions enabled us to prove a stronger version of the tradition
al result. In this case\, the relevant generalisation was to define the co
ncept of nilpotency not just for Lie algebras but for Lie modules also.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Heather Macbeth (Fordham University)
DTSTART;VALUE=DATE-TIME:20220324T160000Z
DTEND;VALUE=DATE-TIME:20220324T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/7
DESCRIPTION:Title: Fourier series\nby Heather Macbeth (Fordham University) as
part of London Learning Lean\n\n\nAbstract\nFourier series are not new to
formalization\; various results were proved by Harrison in HOL Light ten y
ears ago\, and there are developments in Isabelle and Metamath too. But t
he Hilbert space theory and measure theory in Lean's library mathlib allow
s for a very efficient presentation. I will give a tour of some of this t
heory\, touching on topological groups\, the Stone-Weierstrass theorem\, t
he denseness of continuous functions in Lp\, and a TFAE for Hilbert bases.
\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kenny Lau (University of Cambridge)
DTSTART;VALUE=DATE-TIME:20220203T160000Z
DTEND;VALUE=DATE-TIME:20220203T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/8
DESCRIPTION:Title: Tilting Perfectoid Fields\nby Kenny Lau (University of Camb
ridge) as part of London Learning Lean\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nicolò Cavalleri (London School of Geometry and Number Theory)
DTSTART;VALUE=DATE-TIME:20220210T160000Z
DTEND;VALUE=DATE-TIME:20220210T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/9
DESCRIPTION:Title: Topological vector bundles\nby Nicolò Cavalleri (London Sc
hool of Geometry and Number Theory) as part of London Learning Lean\n\nAbs
tract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kexing Ying (Imperial College London)
DTSTART;VALUE=DATE-TIME:20220217T160000Z
DTEND;VALUE=DATE-TIME:20220217T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/10
DESCRIPTION:Title: Probability theory and martingales\nby Kexing Ying (Imperi
al College London) as part of London Learning Lean\n\n\nAbstract\nMartinga
les are stochastic processes in which the conditional expectation of the \
nprocess in the next time step equals the current value. In this seminar I
will \nprovide a brief overview all the definitions required to define an
d work with \nmartingales\, and report on the recent development and chall
enges with \nformalising martingales in Lean.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bhavik Mehta (University of Cambridge)
DTSTART;VALUE=DATE-TIME:20220224T160000Z
DTEND;VALUE=DATE-TIME:20220224T170000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/11
DESCRIPTION:Title: The Erdős-Szemerédi conjecture and working with finiteness\nby Bhavik Mehta (University of Cambridge) as part of London Learning L
ean\n\n\nAbstract\nApproximate groups are a very recent field of study in
arithmetic combinatorics\, studying finite subsets of a fixed group which
are 'almost' closed under multiplication. One of the earliest conjectures
in this area by Erdős and Szemerédi asks whether there is a finite subse
t of reals which is both an approximate additive group\, and an approximat
e multiplicative group: essentially an approximate ring. While the problem
remains open I discuss progress towards it\, and describe the formalisati
on of a 2005 result of Solymosi which gives a partial answer.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jujian Zhang (Imperial College London)
DTSTART;VALUE=DATE-TIME:20220505T150000Z
DTEND;VALUE=DATE-TIME:20220505T160000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/12
DESCRIPTION:Title: Proj\nby Jujian Zhang (Imperial College London) as part of
London Learning Lean\n\nLecture held in Huxley 410\, Department of mathem
atics\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Violeta Hernández Palacios (University of Guanajuato)
DTSTART;VALUE=DATE-TIME:20220512T150000Z
DTEND;VALUE=DATE-TIME:20220512T160000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/13
DESCRIPTION:Title: Ordinals\nby Violeta Hernández Palacios (University of Gu
anajuato) as part of London Learning Lean\n\nLecture held in Huxley 410\,
Department of mathematics\, Imperial College London.\n\nAbstract\nIn under
graduate school\, ordinals are most often dealt with as part of a larger s
et theory course. Many of their basic notions\, up to their definition\, a
re given in set-theoretic terms. Given Lean's type theoretic foundations\,
a new approach is needed to deal with them.\n\nIn this talk\, we discuss
and contrast the von Neumann definition of ordinals with that currently em
ployed in mathlib. By doing so\, we gain insight into basic notions of Lea
n itself\, such as quotients and universes.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/13/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pierre-Alexandre Bazin (ENS Ulm)
DTSTART;VALUE=DATE-TIME:20220519T150000Z
DTEND;VALUE=DATE-TIME:20220519T160000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/14
DESCRIPTION:Title: Classification of finitely-generated modules over a PID\nb
y Pierre-Alexandre Bazin (ENS Ulm) as part of London Learning Lean\n\nLect
ure held in Huxley 410\, Department of mathematics\, Imperial College Lond
on.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Angdinata (London School of Geometry and Number Theory)
DTSTART;VALUE=DATE-TIME:20220526T150000Z
DTEND;VALUE=DATE-TIME:20220526T160000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/15
DESCRIPTION:Title: Elliptic curves and the Mordell-Weil theorem\nby David Ang
dinata (London School of Geometry and Number Theory) as part of London Lea
rning Lean\n\nLecture held in Huxley 410\, Department of mathematics\, Imp
erial College London.\n\nAbstract\nFrom being fundamental objects in numbe
r theory and geometry to seeing new applications in modern cryptosystems a
nd factorisation algorithms\, elliptic curves play a huge role in and out
of mathematics. I will briefly introduce the theory of elliptic curves in
the context of algebraic geometry\, explain the inherent subtlety in provi
ng even the most basic results\, and outline the current status of formali
sation in Lean's mathlib. I will also describe my ongoing attempt to prove
a fundamental result in the number theory of elliptic curves - the Mordel
l-Weil theorem - that the group of rational points of an elliptic curve ov
er a number field is finitely generated.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:No seminar (UK holiday)
DTSTART;VALUE=DATE-TIME:20220602T150000Z
DTEND;VALUE=DATE-TIME:20220602T160000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/16
DESCRIPTION:Title: No seminar (UK holiday)\nby No seminar (UK holiday) as par
t of London Learning Lean\n\nInteractive livestream: https://imperial-ac-u
k.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJlYmRaS01TVlFIRGxtUT09\nLecture held
in Huxley 410\, Department of mathematics\, Imperial College London.\nAbs
tract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/16/
URL:https://imperial-ac-uk.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJlYmRaS01TV
lFIRGxtUT09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sebastian Monnet (London School of Geometry and Number Theory)
DTSTART;VALUE=DATE-TIME:20220609T150000Z
DTEND;VALUE=DATE-TIME:20220609T160000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/17
DESCRIPTION:Title: The Krull Topology\nby Sebastian Monnet (London School of
Geometry and Number Theory) as part of London Learning Lean\n\nInteractive
livestream: https://imperial-ac-uk.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJl
YmRaS01TVlFIRGxtUT09\nLecture held in Huxley 410\, Department of mathemati
cs\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/17/
URL:https://imperial-ac-uk.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJlYmRaS01TV
lFIRGxtUT09
END:VEVENT
BEGIN:VEVENT
SUMMARY:María Inés de Frutos Fernández (Imperial College London)
DTSTART;VALUE=DATE-TIME:20220616T150000Z
DTEND;VALUE=DATE-TIME:20220616T160000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/18
DESCRIPTION:by María Inés de Frutos Fernández (Imperial College London)
as part of London Learning Lean\n\nInteractive livestream: https://imperi
al-ac-uk.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJlYmRaS01TVlFIRGxtUT09\nLectu
re held in Huxley 410\, Department of mathematics\, Imperial College Londo
n.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/18/
URL:https://imperial-ac-uk.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJlYmRaS01TV
lFIRGxtUT09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Yael Dillies (University of Cambridge)
DTSTART;VALUE=DATE-TIME:20220623T150000Z
DTEND;VALUE=DATE-TIME:20220623T160000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/19
DESCRIPTION:by Yael Dillies (University of Cambridge) as part of London Le
arning Lean\n\nInteractive livestream: https://imperial-ac-uk.zoom.us/j/98
307531484?pwd=ejQ3Z2lyaUJlYmRaS01TVlFIRGxtUT09\nLecture held in Huxley 410
\, Department of mathematics\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/19/
URL:https://imperial-ac-uk.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJlYmRaS01TV
lFIRGxtUT09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Wrenna Robson (Royal Holloway)
DTSTART;VALUE=DATE-TIME:20220630T150000Z
DTEND;VALUE=DATE-TIME:20220630T160000Z
DTSTAMP;VALUE=DATE-TIME:20220528T201145Z
UID:LondonLearningLean/20
DESCRIPTION:Title: Post-Quantum Cryptography\nby Wrenna Robson (Royal Hollowa
y) as part of London Learning Lean\n\nInteractive livestream: https://impe
rial-ac-uk.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJlYmRaS01TVlFIRGxtUT09\nLec
ture held in Huxley 410\, Department of mathematics\, Imperial College Lon
don.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/20/
URL:https://imperial-ac-uk.zoom.us/j/98307531484?pwd=ejQ3Z2lyaUJlYmRaS01TV
lFIRGxtUT09
END:VEVENT
END:VCALENDAR