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:20220113T160000Z
DTEND:20220113T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/1
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/1/">Adeles and ideles</a>\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:20220120T160000Z
DTEND:20220120T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/2
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/2/">Modular forms  and Eisenstein series</a>\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:20220127T160000Z
DTEND:20220127T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/3
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/3/">Group cohomology</a>\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:20220303T160000Z
DTEND:20220303T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/4
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/4/">Introduction to matroids</a>\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:20220310T160000Z
DTEND:20220310T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/5
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/5/">p-adic L-functions</a>\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:20220317T160000Z
DTEND:20220317T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/6
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/6/">Engel's theorem in Mathlib</a>\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:20220324T160000Z
DTEND:20220324T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/7
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/7/">Fourier series</a>\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:20220203T160000Z
DTEND:20220203T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/8
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/8/">Tilting Perfectoid Fields</a>\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:20220210T160000Z
DTEND:20220210T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/9
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/9/">Topological vector bundles</a>\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:20220217T160000Z
DTEND:20220217T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/10
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/10/">Probability theory and martingales</a>\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:20220224T160000Z
DTEND:20220224T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/11
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/11/">The Erdős-Szemerédi conjecture and working with finiteness</
 a>\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:20220505T150000Z
DTEND:20220505T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/12
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/12/">Proj</a>\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:20220512T150000Z
DTEND:20220512T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/13
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/13/">Ordinals</a>\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:20220519T150000Z
DTEND:20220519T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/14
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/14/">Classification of finitely-generated modules over a PID</a>\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:20220526T150000Z
DTEND:20220526T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/15
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/15/">Elliptic curves and the Mordell-Weil theorem</a>\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:20220602T150000Z
DTEND:20220602T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/16
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/16/">No seminar (UK holiday)</a>\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:20220609T150000Z
DTEND:20220609T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/17
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/17/">The Krull Topology</a>\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:20220616T150000Z
DTEND:20220616T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/18
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/18/">Extensions of norms and Fontaine’s period rings</a>\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:20220623T150000Z
DTEND:20220623T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/19
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/19/">Behrend's construction and additive combinatorics</a>\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:20220630T150000Z
DTEND:20220630T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/20
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/20/">Post-Quantum Cryptography</a>\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:20230112T160000Z
DTEND:20230112T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/21
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/21/">Ostrowski's theorem</a>\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:20230119T160000Z
DTEND:20230119T170000Z
DTSTAMP:20260421T115916Z
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:20230126T160000Z
DTEND:20230126T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/23
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/23/">Ergodicity and Gallagher's theorem</a>\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:20230202T160000Z
DTEND:20230202T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/24
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/24/">Solving Diophantine equations via the class group</a>\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:20230209T160000Z
DTEND:20230209T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/25
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/25/">Formalising Giles Gardam's disproof of Kaplansky's Unit Conjec
 ture</a>\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:20230216T160000Z
DTEND:20230216T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/26
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/26/">Euler's Totient Theorem and the Prime Number Theorem</a>\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:20230223T160000Z
DTEND:20230223T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/27
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/27/">On the Erdős-Tuza-Valtr Conjecture</a>\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:20230302T160000Z
DTEND:20230302T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/28
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/28/">(speaker illness)</a>\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:20230309T160000Z
DTEND:20230309T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/29
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/29/">Flat modules</a>\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:20230316T160000Z
DTEND:20230316T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/30
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/30/">Some Basics of Gaussian Measure in Lean</a>\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:20230323T160000Z
DTEND:20230323T170000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/31
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/31/">Implementing Cryptographic Primitives in Lean 4</a>\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:20230504T150000Z
DTEND:20230504T160000Z
DTSTAMP:20260421T115916Z
UID:LondonLearningLean/32
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/32/">Tori</a>\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
