BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Sebastian Ullrich (Lean FRO)
DTSTART:20240109T141500Z
DTEND:20240109T144500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/1
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/1/">Are We Fast Yet</a>\nby Sebastian Ullrich (Lean FRO) as part of L
 ean Together 2024\n\n\nAbstract\nA review of Lean performance and benchmar
 king\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rémy Degenne (Univ. Lille\, Inria\, CNRS\, Centrale Lille\, CRISt
 AL)
DTSTART:20240109T144500Z
DTEND:20240109T151500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/2
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/2/">Probability in the formalization of the Polynomial Freiman Ruzsa 
 conjecture</a>\nby Rémy Degenne (Univ. Lille\, Inria\, CNRS\, Centrale Li
 lle\, CRIStAL) as part of Lean Together 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nirvana Coppola
DTSTART:20240109T153000Z
DTEND:20240109T160000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/3
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/3/">Formalization of class numbers computations and Mordell equations
 </a>\nby Nirvana Coppola as part of Lean Together 2024\n\n\nAbstract\nA pr
 oblem of great interest to number theorists is that of finding solutions t
 o Diophantine equations: it is fascinating because it can be formulated in
  a very elementary way\, and yet lead to deep and non trivial mathematics 
 in order to be solved.\nIn this talk I will show how to solve several inst
 ances of the Mordell equation $y^2=x^3+d$ in Lean\, via a descent method t
 hat involves explicit computation of the class number of certain quadratic
  rings. This is joint work with A. Baanen\, A. Best and S. Dahmen.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tomáš Skřivan
DTSTART:20240109T160000Z
DTEND:20240109T163000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/4
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/4/">Automatic differentiation in Lean</a>\nby Tomáš Skřivan as par
 t of Lean Together 2024\n\n\nAbstract\nWe would like to use Lean 4 as a pr
 ogramming language for scientific computing and machine learning. For such
  applications automatic differentiation is a necessary building block. In 
 this talk\, we will present a general function transformation framework th
 at can be used to implement forward and reverse mode automatic differentia
 tion.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dagur Ásgeirsson (University of Copenhagen)
DTSTART:20240109T163000Z
DTEND:20240109T170000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/5
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/5/">Condensed mathematics in Mathlib</a>\nby Dagur Ásgeirsson (Unive
 rsity of Copenhagen) as part of Lean Together 2024\n\n\nAbstract\nCondense
 d mathematics is a new way of studying the interplay between algebra and g
 eometry. It replaces the concept of a topological space by that of a conde
 nsed set\, defined as a sheaf on a certain site of compact Hausdorff space
 s. Parts of this theory were first formalised as part of the Liquid Tensor
  Experiment. In this talk we will discuss formalisation of sheaf theory in
  the context of the process of getting the basic definitions of condensed 
 mathematics into Mathlib.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Emina Torlak (Amazon Web Services)
DTSTART:20240109T171500Z
DTEND:20240109T181500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/6
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/6/">Cedar: A New Language for Expressive\, Fast\, Safe\, and Analyzab
 le Authorization</a>\nby Emina Torlak (Amazon Web Services) as part of Lea
 n Together 2024\n\n\nAbstract\nThis talk presents Cedar\, a new language f
 or authorization that is formalized and verified in Lean.  Cedar is design
 ed to be ergonomic\, fast\, safe\, and analyzable. Cedar’s simple and in
 tuitive syntax supports common authorization use-cases with readable polic
 ies\, leveraging concepts from role-based\, attribute-based\, and relation
 -based access control models. Cedar’s policy structure ensures that acce
 ss requests can be authorized quickly. Its policy validator leverages opti
 onal typing to help policy writers avoid mistakes\, but not get in their w
 ay. Cedar’s design has been finely balanced to enable sound and complete
  policy analysis by reduction to SMT. We have implemented Cedar in Rust an
 d use Lean to formally verify important properties of its design. Cedar is
  used at scale in Amazon Verified Permissions and Amazon Verified Access\,
  and it is freely available at https://github.com/cedar-policy. This talk 
 describes Cedar’s design\, our verification-guided development methodolo
 gy\, and our experience verifying Cedar in Lean.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joël Riou (University Paris-Saclay)
DTSTART:20240110T160000Z
DTEND:20240110T163000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/7
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/7/">Overview of homology in mathlib</a>\nby Joël Riou (University Pa
 ris-Saclay) as part of Lean Together 2024\n\n\nAbstract\nIn this talk\, I 
 will attempt to give an overview of homology in mathlib and discuss plans 
 for future work. For example\, the derived category of an abelian category
  should enter mathlib soon. Total derived functors and spectral sequences 
 shall enter mathlib in a more remote future\, even though most of the code
  already exists in draft form in the mathlib4 branch jriou_localization.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sorawee Porncharoenwase
DTSTART:20240110T163000Z
DTEND:20240110T170000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/8
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/8/">A Pretty Expressive Printer</a>\nby Sorawee Porncharoenwase as pa
 rt of Lean Together 2024\n\n\nAbstract\nPretty printers make trade-offs be
 tween the expressiveness of their pretty printing language\, the optimalit
 y objective that they minimize when choosing between different ways to lay
  out a document\, and the performance of their algorithm.\nThis talk prese
 nts a new pretty printer\, $\\Pi_e$\, that is strictly more expressive tha
 n all pretty printers in the literature and provably minimizes an optimali
 ty objective.\nFurthermore\, the time complexity of $\\Pi_e$ is better tha
 n many existing pretty printers.\nWhen choosing among different ways to la
 y out a document\, $\\Pi_e$ consults a user-supplied cost factory\, which 
 determines the optimality objective\, \ngiving $\\Pi_e$ a unique degree of
  flexibility.\nWe use the Lean theorem prover to verify the correctness (v
 alidity and optimality) of $\\Pi_e$\, and\nimplement $\\Pi_e$ concretely a
 s a pretty printer that we call PrettyExpressive.\nTo evaluate our pretty 
 printer against others\, we develop a formal framework for reasoning about
  the expressiveness of pretty printing languages\, and survey pretty print
 ers in the literature\, comparing their expressiveness\, optimality\, wors
 t-case time complexity\, and practical running time.\nOur evaluation shows
  that PrettyExpressive is efficient and effective at producing optimal lay
 outs. \nPrettyExpressive has also seen real-world adoption: it serves as a
  foundation of a code formatter for Racket.\n\nThis is joint work with Jus
 tin Pombrio and Emina Torlak\, originally published at OOPSLA 2023.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Best (King's College London)
DTSTART:20240110T174500Z
DTEND:20240110T181500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/9
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/9/">Leaff: a Lean library diff tool</a>\nby Alex Best (King's College
  London) as part of Lean Together 2024\n\n\nAbstract\nI'll present the des
 ign and implementation\, and a usage demo\, for a Lean diff tool called Le
 aff.\nThis has at least two potential uses. One is summarising the changes
  to a library's Lean environment over time\, for example when a new commit
  modifies a Lean library\, or when the version of Lean being used to compi
 le the library changes\, the resulting library will be measurably differen
 t\, in ways that are not always apparent from the source changes.\nBut wit
 h Leaff we can get a short summary listing lemmas added and removed\, rena
 mes that took place\, attributes and imports that changed etc.\, which can
  be helpful when reviewing contributions\, or making sure that proposed mo
 difications to Lean don't have unintended downstream consequences.\nThe ot
 her use for this tool is when upgrading dependencies\, the Lean ecosystem 
 is relatively accepting of breaking changes\, normally little backwards co
 mpatibility is maintained over time in mathlib\, Std or in Lean core itsel
 f. This makes the problem of upgrading dependencies time consuming\, if a 
 definition or lemma is moved or renamed\, downstream libraries must be mod
 ified to complete the upgrade\, and disentangling what relevant changes we
 re made can be hard from looking at source commits alone. I'll discuss thi
 s a bit\, and how a future version of this tool may be able to allieviate 
 some such issues completely automatically.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sophie Morel (CNRS/ENS de Lyon)
DTSTART:20240110T181500Z
DTEND:20240110T184500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/10
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/10/">Formalizing Grassmannians in Lean</a>\nby Sophie Morel (CNRS/ENS
  de Lyon) as part of Lean Together 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mac Malone (Lean FRO\, LLC)
DTSTART:20240110T184500Z
DTEND:20240110T191500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/11
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/11/">How Reservoir Boosts Your Lean Packages</a>\nby Mac Malone (Lean
  FRO\, LLC) as part of Lean Together 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ashvni Narayanan (Sydney Mathematical Research Institute\, Univers
 ity of Sydney)
DTSTART:20240110T193000Z
DTEND:20240110T200000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/12
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/12/">p-adic L-functions in Lean</a>\nby Ashvni Narayanan (Sydney Math
 ematical Research Institute\, University of Sydney) as part of Lean Togeth
 er 2024\n\n\nAbstract\nKubota-Leopoldt $p$-adic $L$-functions arise from t
 he study of certain meromorphic functions which have special values at neg
 ative integers relating to Bernoulli numbers. We shall discuss their forma
 lization in Lean 3\, and the subsequent translation to Lean 4.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jireh Loreaux
DTSTART:20240110T200000Z
DTEND:20240110T203000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/13
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/13/">Operator algebras in Mathlib: status and roadmap</a>\nby Jireh L
 oreaux as part of Lean Together 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/13/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrew Yang
DTSTART:20240111T123000Z
DTEND:20240111T130000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/14
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/14/">Fermat’s last theorem for regular primes - Case II</a>\nby And
 rew Yang as part of Lean Together 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Yicheng Qian
DTSTART:20240111T130000Z
DTEND:20240111T133000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/15
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/15/">Auto: An Interface Between Lean and Automated Theorem Provers</a
 >\nby Yicheng Qian as part of Lean Together 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Josh Clune
DTSTART:20240111T133000Z
DTEND:20240111T140000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/16
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/16/">Duper: A Higher-Order Proof Producing Superposition Theorem Prov
 er</a>\nby Josh Clune as part of Lean Together 2024\n\n\nAbstract\nThis ta
 lk will describe Duper\, a piece of general-purpose proof automation for L
 ean 4. The talk will give an overview of how Duper works and will include 
 a short demo showcasing what sorts of problems Duper can and can't automat
 ically solve.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leonidas Lampropoulos (University of Maryland)
DTSTART:20240111T141500Z
DTEND:20240111T144500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/17
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/17/">QuickChick: Property-Based Testing in Coq</a>\nby Leonidas Lampr
 opoulos (University of Maryland) as part of Lean Together 2024\n\nAbstract
 : TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Thrane Christiansen
DTSTART:20240111T151500Z
DTEND:20240111T154500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/18
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/18/">Documentation as a DSL</a>\nby David Thrane Christiansen as part
  of Lean Together 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Wrenna Robson
DTSTART:20240111T163000Z
DTEND:20240111T170000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/19
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/19/">Permutations on bitvectors: an inductive perspective</a>\nby Wre
 nna Robson as part of Lean Together 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jad Elkhaleq Ghalayini (University of Cambridge)
DTSTART:20240112T173000Z
DTEND:20240112T180000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/20
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/20/">Formalizing refinement types in Lean</a>\nby Jad Elkhaleq Ghalay
 ini (University of Cambridge) as part of Lean Together 2024\n\nAbstract: T
 BA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Evgenia Karunus\, Anton Kovsharov
DTSTART:20240111T144500Z
DTEND:20240111T151500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/21
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/21/">Visualising a proof: introducing Paperproof</a>\nby Evgenia Karu
 nus\, Anton Kovsharov as part of Lean Together 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leonardo de Moura
DTSTART:20240112T150000Z
DTEND:20240112T160000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/22
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/22/">Lean FRO meeting</a>\nby Leonardo de Moura as part of Lean Toget
 her 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:María Inés de Frutos Fernández
DTSTART:20240112T161500Z
DTEND:20240112T164500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/23
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/23/">Formalizing local fields in Lean</a>\nby María Inés de Frutos 
 Fernández as part of Lean Together 2024\n\n\nAbstract\nI will discuss a f
 ormalization of complete discrete valuation rings and local fields. This i
 s joint work with Filippo Nuccio.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bhavik Mehta (University of Cambridge)
DTSTART:20240110T170000Z
DTEND:20240110T173000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/24
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/24/">Formalisation of combinatorics</a>\nby Bhavik Mehta (University 
 of Cambridge) as part of Lean Together 2024\n\n\nAbstract\nIn 2023\, a tea
 m of four mathematicians found the first exponential improvement to the up
 per bound in Ramsey's theorem with a paper over 50 pages long. I will disc
 uss this proof and how I formalised it in Lean.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kaiyu Yang (Caltech)
DTSTART:20240111T160000Z
DTEND:20240111T163000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/25
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/25/">Towards Large Language Models as Copilots for Theorem Proving in
  Lean</a>\nby Kaiyu Yang (Caltech) as part of Lean Together 2024\n\n\nAbst
 ract\nWe introduce Lean Copilot to allow large language models (LLMs) to b
 e used in Lean for proof automation\, e.g.\, suggesting tactics/premises a
 nd searching for proofs. You can use our built-in models from LeanDojo or 
 bring your own models that run either locally (w/ or w/o GPUs) or on the c
 loud.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joe Hendrix
DTSTART:20240112T180000Z
DTEND:20240112T183000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/26
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/26/">Standard Library 2024</a>\nby Joe Hendrix as part of Lean Togeth
 er 2024\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/26/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Patrick Massot
DTSTART:20240109T140000Z
DTEND:20240109T141500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/27
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/27/">Welcome</a>\nby Patrick Massot as part of Lean Together 2024\n\n
 Abstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Coffee break
DTSTART:20240109T151500Z
DTEND:20240109T153000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/28
DESCRIPTION:by Coffee break as part of Lean Together 2024\n\nAbstract: TBA
 \n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Coffee break
DTSTART:20240109T170000Z
DTEND:20240109T171500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/29
DESCRIPTION:by Coffee break as part of Lean Together 2024\n\nAbstract: TBA
 \n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social hour
DTSTART:20240109T181500Z
DTEND:20240109T191500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/30
DESCRIPTION:by Social hour as part of Lean Together 2024\n\nAbstract: TBA\
 n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Coffee break
DTSTART:20240110T173000Z
DTEND:20240110T174500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/31
DESCRIPTION:by Coffee break as part of Lean Together 2024\n\nAbstract: TBA
 \n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Coffee break
DTSTART:20240110T191500Z
DTEND:20240110T193000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/32
DESCRIPTION:by Coffee break as part of Lean Together 2024\n\nAbstract: TBA
 \n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/32/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social hour
DTSTART:20240110T203000Z
DTEND:20240110T213000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/33
DESCRIPTION:by Social hour as part of Lean Together 2024\n\nAbstract: TBA\
 n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/33/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Coffee break
DTSTART:20240111T140000Z
DTEND:20240111T141500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/34
DESCRIPTION:by Coffee break as part of Lean Together 2024\n\nAbstract: TBA
 \n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/34/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Coffee break
DTSTART:20240111T154500Z
DTEND:20240111T160000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/35
DESCRIPTION:by Coffee break as part of Lean Together 2024\n\nAbstract: TBA
 \n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/35/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social hour
DTSTART:20240111T170000Z
DTEND:20240111T180000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/36
DESCRIPTION:by Social hour as part of Lean Together 2024\n\nAbstract: TBA\
 n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/36/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Coffee break
DTSTART:20240112T160000Z
DTEND:20240112T161500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/37
DESCRIPTION:by Coffee break as part of Lean Together 2024\n\nAbstract: TBA
 \n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/37/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Coffee break
DTSTART:20240112T171500Z
DTEND:20240112T173000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/38
DESCRIPTION:by Coffee break as part of Lean Together 2024\n\nAbstract: TBA
 \n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/38/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social hour
DTSTART:20240112T183000Z
DTEND:20240112T193000Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/39
DESCRIPTION:by Social hour as part of Lean Together 2024\n\nAbstract: TBA\
 n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/39/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ramon Fernández Mir (University of Edinburgh)
DTSTART:20240112T164500Z
DTEND:20240112T171500Z
DTSTAMP:20260406T001557Z
UID:LeanTogether2024/40
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LeanTogether
 2024/40/">CvxLean: modeling convex optimization problems in Lean</a>\nby R
 amon Fernández Mir (University of Edinburgh) as part of Lean Together 202
 4\n\n\nAbstract\nMany practical problems in engineering can be phrased as 
 optimization problems. If the problem has a convex formulation\, then it c
 an often be reduced and solved efficiently. Our tool verifies the reductio
 n of the original problem into its solver-compatible form and provides an 
 environment for users to transform optimization problems interactively. In
  this talk\, we will give some motivating examples and show CvxLean's newe
 st features.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2024/40/
END:VEVENT
END:VCALENDAR