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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
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:20240222T212509Z
UID:LondonLearningLean/16
DESCRIPTION:Title: No seminar (UK holiday)\nby No seminar (UK holiday) as par
t of London Learning Lean\n\nLecture held in Huxley 410\, Department of ma
thematics\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/16/
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:20240222T212509Z
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\nLecture hel
d in Huxley 410\, Department of mathematics\, Imperial College London.\nAb
stract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/17/
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:20240222T212509Z
UID:LondonLearningLean/18
DESCRIPTION:Title: Extensions of norms and Fontaine’s period rings\nby Mar
ía Inés de Frutos Fernández (Imperial College London) as part of London
Learning Lean\n\nLecture held in Huxley 410\, Department of mathematics\,
Imperial College London.\n\nAbstract\nLet $K$ be a field complete with re
spect to a nonarchimedean real-valued norm\, and let $L/K$ be an algebraic
extension. We show that there is a unique norm on $L$ extending the given
norm on $K$\, of which we give an explicit description. As an application
\, we extend the $p$-adic norm on $\\mathbb{Q}_p$ to $\\mathbb{Q}_p^{\\tex
t{alg}}$ and define its completion $\\mathbb{C}_p$. Building on the defini
tion of $\\mathbb{C}_p$\, we formalize the definitions of the Fontaine's p
eriod rings $B_{\\text{dR}}$ and $B_{\\text{HT}}$.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Yael Dillies (University of Cambridge)
DTSTART;VALUE=DATE-TIME:20220623T150000Z
DTEND;VALUE=DATE-TIME:20220623T160000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/19
DESCRIPTION:Title: Behrend's construction and additive combinatorics\nby Yael
Dillies (University of Cambridge) 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/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Wrenna Robson (Royal Holloway)
DTSTART;VALUE=DATE-TIME:20220630T150000Z
DTEND;VALUE=DATE-TIME:20220630T160000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/20
DESCRIPTION:Title: Post-Quantum Cryptography\nby Wrenna Robson (Royal Hollowa
y) as part of London Learning Lean\n\nLecture held in Huxley 410\, Departm
ent of mathematics\, Imperial College London.\n\nAbstract\nA discussion of
the post-quantum cryptography zoo\, and some thoughts on how hard it migh
t be to formalise the relevant mathematics into Lean.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Billy Miao (Imperial College London)
DTSTART;VALUE=DATE-TIME:20230112T160000Z
DTEND;VALUE=DATE-TIME:20230112T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/21
DESCRIPTION:Title: Ostrowski's theorem\nby Billy Miao (Imperial College Londo
n) as part of London Learning Lean\n\nLecture held in Huxley 410\, Departm
ent of mathematics\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ashvni Narayanan (LSGNT/Imperial College London)
DTSTART;VALUE=DATE-TIME:20230119T160000Z
DTEND;VALUE=DATE-TIME:20230119T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/22
DESCRIPTION:by Ashvni Narayanan (LSGNT/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/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Oliver Nash (Imperial College London)
DTSTART;VALUE=DATE-TIME:20230126T160000Z
DTEND;VALUE=DATE-TIME:20230126T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/23
DESCRIPTION:Title: Ergodicity and Gallagher's theorem\nby Oliver Nash (Imperi
al College London) as part of London Learning Lean\n\nLecture held in Huxl
ey 410\, Department of mathematics\, Imperial College London.\nAbstract: T
BA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Best (Vrije Universiteit Amsterdam)
DTSTART;VALUE=DATE-TIME:20230202T160000Z
DTEND;VALUE=DATE-TIME:20230202T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/24
DESCRIPTION:Title: Solving Diophantine equations via the class group\nby Alex
Best (Vrije Universiteit Amsterdam) as part of London Learning Lean\n\nLe
cture held in Huxley 410\, Department of mathematics\, Imperial College Lo
ndon.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Anand Rao Tadipatri + Siddhartha Gadgil (IISc)
DTSTART;VALUE=DATE-TIME:20230209T160000Z
DTEND;VALUE=DATE-TIME:20230209T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/25
DESCRIPTION:Title: Formalising Giles Gardam's disproof of Kaplansky's Unit Conjec
ture\nby Anand Rao Tadipatri + Siddhartha Gadgil (IISc) as part of Lon
don Learning Lean\n\nLecture held in Huxley 410\, Department of mathematic
s\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ella Yu + Xiang Li (Imperial College London / University of Cambri
dge)
DTSTART;VALUE=DATE-TIME:20230216T160000Z
DTEND;VALUE=DATE-TIME:20230216T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/26
DESCRIPTION:Title: Euler's Totient Theorem and the Prime Number Theorem\nby E
lla Yu + Xiang Li (Imperial College London / University of Cambridge) as p
art of London Learning Lean\n\nLecture held in Huxley 410\, Department of
mathematics\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/26/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jineon Baek (University of Michigan)
DTSTART;VALUE=DATE-TIME:20230223T160000Z
DTEND;VALUE=DATE-TIME:20230223T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/27
DESCRIPTION:Title: On the Erdős-Tuza-Valtr Conjecture\nby Jineon Baek (Unive
rsity of Michigan) as part of London Learning Lean\n\nLecture held in Huxl
ey 410\, Department of mathematics\, Imperial College London.\n\nAbstract\
nThe Erdős-Szekeres conjecture states that any set of more than $2^{n-2}$
points in the plane with no three on a line contains the vertices of a co
nvex n-gon. Later\, Erdős\, Tuza and Valtr strengthened the conjecture by
stating that any set of more than $\\sum_{i = n + 2 - b}^{a} \\binom{n -
2}{i - 2}$ points in a plane either contains the vertices of a convex n-go
n\, a points lying on an upwardly convex curve\, or b points lying on a do
wnwardly convex curve. They also showed that the generalization is actuall
y equivalent to the Erdős-Szekeres conjecture. \nWe prove the first new c
ase $a = 4\, b = n$ of the Erdős-Tuza-Valtr conjecture since the original
1935 paper of Erdős and Szekeres. Namely\, we show that any set of $(n-1
)(n-2)/2 + 2$ points in the plane with no three points on a line and no tw
o points sharing the same x-coordinate either contains a 4-cap or the vert
ices of a convex n-gon. The proof is fully formalized in Lean 3\, and we w
ill discuss its implementation: structure and API choices\, unexpected pro
blems arised in formalization\, etc.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:cancelled (LSGNT/Kings College London)
DTSTART;VALUE=DATE-TIME:20230302T160000Z
DTEND;VALUE=DATE-TIME:20230302T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/28
DESCRIPTION:Title: (speaker illness)\nby cancelled (LSGNT/Kings College Londo
n) as part of London Learning Lean\n\nLecture held in Huxley 410\, Departm
ent of mathematics\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jujian Zhang (LSGNT/Imperial College)
DTSTART;VALUE=DATE-TIME:20230309T160000Z
DTEND;VALUE=DATE-TIME:20230309T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/29
DESCRIPTION:Title: Flat modules\nby Jujian Zhang (LSGNT/Imperial College) as
part of London Learning Lean\n\nLecture held in Huxley 410\, Department of
mathematics\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joy Hu/Runchang Li (Imperial College London)
DTSTART;VALUE=DATE-TIME:20230316T160000Z
DTEND;VALUE=DATE-TIME:20230316T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/30
DESCRIPTION:Title: Some Basics of Gaussian Measure in Lean\nby Joy Hu/Runchan
g Li (Imperial College London) as part of London Learning Lean\n\nLecture
held in Huxley 410\, Department of mathematics\, Imperial College London.\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Matej Penciak (Yatima/Lurk Lab)
DTSTART;VALUE=DATE-TIME:20230323T160000Z
DTEND;VALUE=DATE-TIME:20230323T170000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/31
DESCRIPTION:Title: Implementing Cryptographic Primitives in Lean 4\nby Matej
Penciak (Yatima/Lurk Lab) as part of London Learning Lean\n\n\nAbstract\nA
bstract: In this talk I will describe the experience of using Lean 4 as a
fully-fledged programming language to implement various number theoretic p
rimitives used in cryptography. In particular\, we will go through the exa
mples of efficient implementations of finite field arithmetic\, fast ellip
tic curve group operations\, and some commonly used cryptographic hash fun
ctions. Along the way I plan on reflecting on the lessons learned in build
ing structurally and mathematically complex libraries in Lean 4. I will al
so cover some future directions and long-term visions of Lean 4's place in
modern cryptography.\n\nNote: this talk will be *online only*\; there is
no room booked for this week.\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Amelia Livingston (London School of Geometry and Number Theory)
DTSTART;VALUE=DATE-TIME:20230504T150000Z
DTEND;VALUE=DATE-TIME:20230504T160000Z
DTSTAMP;VALUE=DATE-TIME:20240222T212509Z
UID:LondonLearningLean/32
DESCRIPTION:Title: Tori\nby Amelia Livingston (London School of Geometry and
Number Theory) as part of London Learning Lean\n\nLecture held in Huxley 4
10\, Department of mathematics\, Imperial College London.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/32/
END:VEVENT
END:VCALENDAR