BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Jireh Loreaux (Southern Illinois University Edwardsville)
DTSTART:20250114T140000Z
DTEND:20250114T141500Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/1
DESCRIPTION:Title: Welcome\nby Jireh Loreaux (Southern Illinois Universit
y Edwardsville) as part of Lean Together 2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jason Rute (IBM Research)
DTSTART:20250115T150000Z
DTEND:20250115T153000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/2
DESCRIPTION:Title: The last mile: How do we make AI theorem provers which wor
k in the real world for real users and not just on benchmarks?\nby Jas
on Rute (IBM Research) as part of Lean Together 2025\n\n\nAbstract\nAs AI
research progresses\, we are seeing massive gains on formal math benchmark
s like MiniF2F and challenges like the IMO. However\, these gains are not
directly accessible to the typical ITP user\, nor are they used to build
formal mathematical libraries. Is this because the technology is not as g
ood as promised or because there is a disconnect between research and the
day-to-day needs of users? I propose that even today\, we have sufficient
AI technology to enhance the experience of proof assistant users signific
antly. I approach this from the lens of product-focused software engineer
ing. How do we bridge “the last mile” to make a useful product for th
e end user?\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Damiano Testa (University of Warwick)
DTSTART:20250114T144500Z
DTEND:20250114T151500Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/3
DESCRIPTION:Title: An introduction to linters\nby Damiano Testa (Universi
ty of Warwick) as part of Lean Together 2025\n\n\nAbstract\nThis is a shor
t introduction to linters and their uses.\n\nThe talk assumes some basic f
amiliarity with Lean.\n\nI will use the linters in Mathlib as main source
of examples.\n\nHowever\, no previous knowledge of linters is required!\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Xavier Généreux and Jannis Limperg (University of Munich (LMU))
DTSTART:20250114T151500Z
DTEND:20250114T154500Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/4
DESCRIPTION:Title: Efficient Forward Reasoning for Aesop\nby Xavier Gén
éreux and Jannis Limperg (University of Munich (LMU)) as part of Lean Tog
ether 2025\n\n\nAbstract\nAesop\, a white-box proof search tactic for Lean
\, has long supported forward rules\, which derive additional facts from t
he hypotheses in a goal. However\, the initial implementation of this feat
ure did not scale to local contexts containing many hypotheses. A core lim
itation of the initial implementation was that it was stateless and so had
to redo large amounts of work on each goal that Aesop produced\, even tho
ugh the local contexts of these goals tend to be very similar.\n\nWe prese
nt a new\, stateful implementation that takes advantage of such similariti
es to achieve much better performance on various examples. The new impleme
ntation is almost fully backwards compatible and is already Aesop's defaul
t. We will also discuss some ideas for how forward rules can be used to bu
ild effective Aesop rule sets.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Emily Riehl (Johns Hopkins University)
DTSTART:20250114T160000Z
DTEND:20250114T163000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/5
DESCRIPTION:Title: The ∞-cosmos project: formalizing 1-\, 2-\, V-\, and ∞
-category theory in Lean\nby Emily Riehl (Johns Hopkins University) as
part of Lean Together 2025\n\n\nAbstract\nThe ∞-cosmos project aims to
leverage the existing libraries developing 1-category theory\, 2-category
theory\, and enriched (V-)category theory in Lean to formalize basic ∞-c
ategory theory. After giving a high-level overview of the problem\, plan\,
and progress of the project (so far)\, we illustrate some challenges rela
ted to the formalization of the supporting results from 1-category theory\
, 2-category theory\, and enriched (V-)category theory that we have encoun
tered thus far in hopes of attracting interest from folks who want to help
us solve them.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Weber\, Vlad Tsyrklevich
DTSTART:20250114T163000Z
DTEND:20250114T171500Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/6
DESCRIPTION:Title: Equational Theories Project\nby Daniel Weber\, Vlad Ts
yrklevich as part of Lean Together 2025\n\n\nAbstract\nOn Sep 25\, 2024\,
Terence Tao announced a project to research a problem in universal algebra
\, using Lean to formalize the results. The goal of the project is to clas
sify the relationship between all equational theories of magmas in a singl
e equation of up to order 4 (magmas are sets with a closed binary operatio
n with no additional structure.) The project also has the additional aim o
f exploring new ways of researching mathematics collaboratively. This talk
describes some of the aims\, methods\, and results of the project.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lean FRO (Lean FRO)
DTSTART:20250114T173000Z
DTEND:20250114T183000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/7
DESCRIPTION:Title: The Lean FRO Year 2 Roadmap and Vision\nby Lean FRO (L
ean FRO) as part of Lean Together 2025\n\n\nAbstract\nThe Lean Focused Res
earch Organization (FRO) envisions a future where Lean becomes a pivotal t
ool for driving innovation and progress across diverse fields. Our vision
encompasses formal mathematics\, software and hardware verification\, soft
ware development\, AI research for mathematics and code synthesis\, as wel
l as new methodologies for math and computer science education. In this ta
lk\, we will present the Lean FRO's progress to date\, outline our roadmap
for Year 2\, and introduce new team members. We will also explore key ini
tiatives aimed at enhancing Lean's scalability\, usability\, proof automat
ion\, and documentation.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Renshaw
DTSTART:20250114T183000Z
DTEND:20250114T190000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/8
DESCRIPTION:Title: Searching for Proof Improvements with tryAtEachStep\nb
y David Renshaw as part of Lean Together 2025\n\n\nAbstract\nI will presen
t tryAtEachStep\, a tool that walks through Lean source code and runs a gi
ven tactic on every proof step. I will discuss how it is implemented\, a v
ariety of different ways it might be used\, and some results from running
it on Mathlib.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Scott Carnahan (University of Tsukuba)
DTSTART:20250115T123000Z
DTEND:20250115T130000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/9
DESCRIPTION:Title: Vertex algebras in Mathlib: coming soon?\nby Scott Car
nahan (University of Tsukuba) as part of Lean Together 2025\n\n\nAbstract\
nVertex algebras appear naturally in the representation theory of Lie alge
bras and finite groups\, but they have a reputation for unwieldy complexit
y. In order to work with them efficiently\, one typically manipulates form
al power series in multiple variables. I will describe some progress towar
d implementing the necessary theory in Mathlib\, and some of the upcoming
challenges.\n\nThis talk will not assume any knowledge of representation t
heory or Lie algebras.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Siddhartha Gadgil (Indian Institute of Science\, Bangalore)
DTSTART:20250115T130000Z
DTEND:20250115T133000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/10
DESCRIPTION:Title: Real world Autoformalization\nby Siddhartha Gadgil (I
ndian Institute of Science\, Bangalore) as part of Lean Together 2025\n\n\
nAbstract\nAutoformalization shows great promise both in helping formalize
mathematics and in allowing mathematicians to use the combination of AI a
nd Lean without expertise in either. We have been working towards realizin
g this promise\, focussing on both improving Autoformalization and on tool
ing and integration with Lean.\n\nHere I will discuss some of our efforts
and techniques that help with autoformalization and with making it usable.
\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jakob von Raumer (Lindy Labs)
DTSTART:20250115T133000Z
DTEND:20250115T140000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/11
DESCRIPTION:Title: Building a Formal Verification Framework for Smart Contra
cts\nby Jakob von Raumer (Lindy Labs) as part of Lean Together 2025\n\
n\nAbstract\nIn the past two years I have been building a formal verficati
on tool called Aegis and used it to verify smart contracts on the Starknet
blockchain. In my talk I will describe the challenges and the joy of buil
ding a lightweight Lean package that enables a slick verification workflow
.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250115T140000Z
DTEND:20250115T143000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/12
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joseph Rotella
DTSTART:20250115T143000Z
DTEND:20250115T150000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/13
DESCRIPTION:Title: Programming with Dependently Typed Tables in Lean\nby
Joseph Rotella as part of Lean Together 2025\n\n\nAbstract\nIn this talk\
, I will present a Lean library for programming with tabular data. Tables
challenge many type systems due to their heterogeneity and the need for ty
pe-level computations to express many common table operations—challenges
to which Lean's dependent type system is well suited. I will discuss the
design\, implementation\, and verification of this library following the B
rown Benchmark for Table Types\, a benchmark based on existing tabular pro
gramming frameworks.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Oliver Nash (Google DeepMind)
DTSTART:20250114T141500Z
DTEND:20250114T144500Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/14
DESCRIPTION:Title: Root systems and root data in Mathlib\nby Oliver Nash
(Google DeepMind) as part of Lean Together 2025\n\n\nAbstract\nI will dis
cuss the formalisation of root systems and root data in Lean's mathematics
library\, Mathlib. These structures provide a good example of the idiom t
hat "good definitions are hard work". In this case\, part of the challenge
is to have a single definition that simultaneously specialises to root sy
stems\, root data\, works in any characteristic\, and also permits a theor
y of infinite root systems (such as the roots of a Kac-Moody algebra).\n\n
The mathematical content will be elementary\, and the emphasis will be on
the lessons for computer formalisation.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250115T153000Z
DTEND:20250115T160000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/15
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Henrik Böving (Lean FRO)
DTSTART:20250115T160000Z
DTEND:20250115T163000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/16
DESCRIPTION:Title: Automated Bit-Level Reasoning in Lean 4\nby Henrik B
öving (Lean FRO) as part of Lean Together 2025\n\n\nAbstract\nThis talk w
ill describe bv_decide\, a tactic for solving all fixed-width BitVec goals
.\nIt will give an overview of the inner workings of bv_decide as well as
a performance evaluation\, showcasing\nsome applications of bv_decide to r
eal world problems.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lorenzo Luccioli (University of Bologna)
DTSTART:20250115T163000Z
DTEND:20250115T170000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/17
DESCRIPTION:Title: Information theory in Lean: the DPI\nby Lorenzo Lucci
oli (University of Bologna) as part of Lean Together 2025\n\n\nAbstract\nT
he Data Processing Inequality (DPI) is a cornerstone of information theory
\, expressing the principle that information cannot be created through pro
cessing.\n\nIn this talk\, I will present the formalization of information
-theoretic results carried out by Rémy Degenne and myself using the Lean
4 theorem prover. The focus will be on the formalization of information di
vergences—particularly f-divergences—and their associated Data Process
ing Inequality (DPI)\, along with their connection to the framework of hyp
othesis testing. I will also discuss the key challenges and design decisio
ns faced during the project.\n
LOCATION:https://master.researchseminars.org/talk/LeanTogether2025/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Violeta Hernández Palacios (Universidad de Guanajuato)
DTSTART:20250115T170000Z
DTEND:20250115T173000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/18
DESCRIPTION:Title: A Nimble Introduction to Nimbers\nby Violeta Hernánd
ez Palacios (Universidad de Guanajuato) as part of Lean Together 2025\n\n\
nAbstract\nJohn Horton Conway first defined the field of "nimbers" in 1976
. This seemingly innocuous structure arising from the combinatorial game o
f Nim turns out to have surprisingly deep structure\, and nearly five deca
des later there are still major open problems.\n\nOne of the most surprisi
ng results on nimbers is that they form an algebraically complete field. T
his talk will focus on the mathematics required to arrive at this result a
nd the ongoing project to formalize them in Lean 4.\n\nThis talk will not
assume prior knowledge of nimbers\, though it will assume some basic famil
iarity with ordinal numbers.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Michael Rothgang (Universität Bonn)
DTSTART:20250116T160000Z
DTEND:20250116T163000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/19
DESCRIPTION:Title: Scaling mathlib: tooling and automation for an ever-growi
ng mathematics library\nby Michael Rothgang (Universität Bonn) as par
t of Lean Together 2025\n\n\nAbstract\nMaintaining the mathlib library in
the presence of continuous growth is a challenge in many aspects.\nOn a te
chnical level\, this relies on a fair amount of custom tooling and automat
ion to keep things manageable. I will highlight some recent additions in a
reas such as deprecations\, linting\, bots and a new review dashboard.\nTh
is involves work by many people\, including Damiano Testa\, Johan Commelin
\, Mario Carneiro and the author.\n\nThis talk is mostly aimed at mathlib
contributors (and reviewers)\, but there will be useful information for ma
thlib users also.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250116T163000Z
DTEND:20250116T170000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/20
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Floris van Doorn (University of Bonn)
DTSTART:20250116T170000Z
DTEND:20250116T173000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/21
DESCRIPTION:Title: Progress report on the Carleson Project\nby Floris va
n Doorn (University of Bonn) as part of Lean Together 2025\n\n\nAbstract\n
I will give a progress report on the Carleson project\, an ongoing formali
zation project of a generalization of Carleson's theorem\, a major result
in harmonic analysis.\n\nI will describe the mathematical ideas in the gen
eralized results\, the status of the project and some reflections of the c
ollaborative nature of the project.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Marcus Rossel
DTSTART:20250116T173000Z
DTEND:20250116T180000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/22
DESCRIPTION:Title: Egg: An Equality Saturation Tactic in Lean\nby Marcus
Rossel as part of Lean Together 2025\n\n\nAbstract\nRewriting is an extre
mely common proof task supported by efficient and versatile tactics like $
\\texttt{rw}$ and $\\texttt{simp}$. These tactics are\, however\, limiting
in that users need to either provide an explicit order and direction of r
ewrites\, or rely on a fixed simplification direction. In our talk\, we pr
esent a new (work in progress) tactic for rewriting using equality saturat
ion. This approach allows us to tackle goals which are infeasible for $\\t
exttt{simp}$ without requiring the details needed for $\\texttt{rw}$.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social hour
DTSTART:20250116T180000Z
DTEND:20250116T183000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/23
DESCRIPTION:Title: Gather Town\nby Social hour as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jean-Baptiste Tristan (Amazon)
DTSTART:20250116T183000Z
DTEND:20250116T190000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/24
DESCRIPTION:Title: Verified Foundations for Differential Privacy\nby Jea
n-Baptiste Tristan (Amazon) as part of Lean Together 2025\n\n\nAbstract\nD
ifferential privacy (DP) has become the gold standard for privacy-preservi
ng data analysis\, but implementing it correctly has proven challenging. P
rior work has focused on verifying DP at a high level\, assuming the found
ations are correct and a perfect source of randomness is available. Howeve
r\, the underlying theory of differential privacy can be very complex and
subtle. Flaws in basic mechanisms and random number generation have been a
critical source of vulnerabilities in real-world DP systems.\n\nIn this t
alk\, we present SampCert\, the first comprehensive\, mechanized foundatio
n for differential privacy. SampCert is written in Lean with over 12\,000
lines of proof. It offers a generic and extensible notion of DP\, a framew
ork for constructing and composing DP mechanisms\, and formally verified i
mplementations of Laplace and Gaussian sampling algorithms. SampCert provi
des (1) a mechanized foundation for developing the next generation of diff
erentially private algorithms\, and (2) mechanically verified primitives t
hat can be deployed in production systems. Indeed\, SampCert’s verified
algorithms power the DP offerings of Amazon Web Services (AWS)\, demonstra
ting its real-world impact.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Abdalrhman Mohamed (Stanford University)
DTSTART:20250116T190000Z
DTEND:20250116T193000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/25
DESCRIPTION:Title: lean-SMT\nby Abdalrhman Mohamed (Stanford University)
as part of Lean Together 2025\n\n\nAbstract\nIn this talk\, I will presen
t lean-SMT\, a tactic designed to discharge Lean goals using SMT solvers.
The tactic translates the negation of a Lean goal into an SMT query and se
nds it to cvc5\, a proof-producing SMT solver. If cvc5 determines the quer
y to be unsatisfiable\, its proof is reconstructed and replayed within Lea
n.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250116T193000Z
DTEND:20250116T200000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/26
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jack McKoen (University of Alberta)
DTSTART:20250116T200000Z
DTEND:20250116T203000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/27
DESCRIPTION:Title: Toward functor quasi-categories in Lean\nby Jack McKo
en (University of Alberta) as part of Lean Together 2025\n\n\nAbstract\nI
will discuss my ongoing formalization of basic ∞-category theory (adjace
nt to the ∞-cosmos project). In particular\, I have been formalizing a p
roof that the internal hom between quasi-categories is again a quasi-categ
ory—an important result toward the Yoneda lemma (for example). I will br
iefly go over the proof\, the ingredients that make it work\, and the API
I've been working on: lifting problems\, weakly saturated classes\, the ge
neration of certain classes of morphisms\, simplicial subsets\, etc. I'll
explain what's been done so far and what's left to do.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Kontorovich (Rutgers University)
DTSTART:20250117T150000Z
DTEND:20250117T153000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/28
DESCRIPTION:Title: Complex Analysis and PrimeNumberTheorem+ in Lean\nby
Alex Kontorovich (Rutgers University) as part of Lean Together 2025\n\n\nA
bstract\nWe will report on some experiments with using formalization for l
arge scale collaboration.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Christian Merten (Utrecht University)
DTSTART:20250117T153000Z
DTEND:20250117T160000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/29
DESCRIPTION:Title: Formalizing the Bruhat-Tits tree\nby Christian Merten
(Utrecht University) as part of Lean Together 2025\n\n\nAbstract\nThe Bru
hat-Tits tree of $SL_2$ of a local field is an important tool in number th
eory and\na very special case of a Bruhat-Tits building\, which are analog
ues of real symmetric spaces in the p-adic world. In this talk\, I will ou
tline its construction in the proof assistant Lean 4 and explain some of t
he challenges and design decisions that appeared in the process.\n\nThis i
s joint work with Judith Ludwig.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250117T160000Z
DTEND:20250117T163000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/30
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hannah Fechtner (Carnegie Mellon University)
DTSTART:20250117T163000Z
DTEND:20250117T170000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/31
DESCRIPTION:Title: Braid Groups in Lean\nby Hannah Fechtner (Carnegie Me
llon University) as part of Lean Together 2025\n\n\nAbstract\nBraids can b
e defined topologically (think: intertwined strings in space) or algebraic
ally in terms of generators and relations. I will discuss the algebraic de
finition\, and its formalization in Lean. \n\nThe word problem in the brai
d group is decidable\, and the larger\, ongoing project is to implement a
verified algorithm\, following Dehornoy. I will discuss the formalization
of the first major stage: defining the braid monoid and embedding it into
the braid group. While formalizing the remaining portion\, I noticed visua
l intuition sneaking into the termination/correctness proof for this algor
ithm. I will present a novel pen-and-paper proof which can rescue the clai
m. \n\nLastly\, I will briefly share a peek at a braid visualization widge
t-to-come!\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joseph Tooby-Smith (Reykjavik University)
DTSTART:20250117T170000Z
DTEND:20250117T173000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/32
DESCRIPTION:Title: Physics and Lean\nby Joseph Tooby-Smith (Reykjavik Un
iversity) as part of Lean Together 2025\n\n\nAbstract\nThis talk explores
the formalization of physics within Lean. I will present my long-term visi
on of what such a formalization should look in 10 years and introduce HepL
ean\, a project which is a step towards this goal. My aim is give the audi
ence 'food for thought' about the progress being made\, the challenges tha
t lie ahead\, and how the community can contribute to the formalization of
physics.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Kurniadi Angdinata (London School of Geometry and Number The
ory)
DTSTART:20250117T173000Z
DTEND:20250117T180000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/33
DESCRIPTION:Title: Division polynomials of elliptic curves\nby David Kur
niadi Angdinata (London School of Geometry and Number Theory) as part of L
ean Together 2025\n\n\nAbstract\nElliptic curves are one of the simplest n
on-trivial objects in algebraic geometry and are pervasive in modern numbe
r theory such as in Wiles's proof of Fermat's last theorem. Their points f
orm an abelian group under a geometric addition law given by explicit rati
onal functions. In particular\, there is an explicit formula for the multi
plication of a point by $ n $ in terms of certain inductively-defined divi
sion polynomials\, which are crucial in point counting algorithms and publ
ic key cryptography. In this talk\, I will explain our formalisation of di
vision polynomials and the multiplication-by-$ n $ formula\, whose proof t
urned out to be quite elusive. This is joint work with Junyan Xu.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Yuma Mizuno (University College Dublin)
DTSTART:20250117T180000Z
DTEND:20250117T183000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/34
DESCRIPTION:Title: Metaprogramming on monoidal categories\nby Yuma Mizun
o (University College Dublin) as part of Lean Together 2025\n\n\nAbstract\
nI will introduce the string diagram widget and the coherence tactic. The
string diagram widget is a tool designed to visualize morphisms in monoida
l categories or 2-morphisms in bicategories. The coherence tactic is a tac
tic for proving coherence conditions within monoidal categories or bicateg
ories. I will explain how these tools have been implemented using metaprog
ramming in Lean.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leni Aniva (Stanford University Centaur Lab)
DTSTART:20250116T203000Z
DTEND:20250116T210000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/35
DESCRIPTION:Title: Pantograph: A Machine-to-Machine Interaction Interface fo
r Lean 4\nby Leni Aniva (Stanford University Centaur Lab) as part of L
ean Together 2025\n\n\nAbstract\nIn this paper\, we introduce Pantograph\,
a tool that provides a versatile interface to the Lean 4 proof assistant
and enables efficient proof search via powerful search algorithms such as
Monte Carlo Tree Search. Pantograph enables high-level reasoning by allowi
ng the user to control Lean 4's inference steps. We provide an overview of
Pantograph's architecture and features. We also report on an illustrative
use case: using machine learning models and proof sketches to prove Lean
4 theorems. Pantograph's innovative features pave the way for more advance
d machine learning models to perform complex proof searches and high-level
reasoning\, equipping future researchers to design more versatile and pow
erful theorem provers.\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250114T154500Z
DTEND:20250114T160000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/36
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250114T171500Z
DTEND:20250114T173000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/37
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250114T190000Z
DTEND:20250114T193000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/38
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250117T183000Z
DTEND:20250117T193000Z
DTSTAMP:20260513T154430Z
UID:LeanTogether2025/39
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together
2025\n\nAbstract: TBA\n
LOCATION:
END:VEVENT
END:VCALENDAR