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:20260428T193228Z
UID:LeanTogether2025/1
DESCRIPTION:Title: Welcome\nby Jireh Loreaux (Southern Illinois University Edwar
dsville) as part of Lean Together 2025\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jason Rute (IBM Research)
DTSTART:20250115T150000Z
DTEND:20250115T153000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/2
DESCRIPTION:Title: The last mile: How do we make AI theorem provers which work in th
e real world for real users and not just on benchmarks?\nby Jason Rute
(IBM Research) as part of Lean Together 2025\n\n\nAbstract\nAs AI researc
h progresses\, we are seeing massive gains on formal math benchmarks like
MiniF2F and challenges like the IMO. However\, these gains are not direct
ly accessible to the typical ITP user\, nor are they used to build formal
mathematical libraries. Is this because the technology is not as good 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 tec
hnology to enhance the experience of proof assistant users significantly.
I approach this from the lens of product-focused software engineering. H
ow do we bridge “the last mile” to make a useful product for the end u
ser?\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Damiano Testa (University of Warwick)
DTSTART:20250114T144500Z
DTEND:20250114T151500Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/3
DESCRIPTION:Title: An introduction to linters\nby Damiano Testa (University of W
arwick) as part of Lean Together 2025\n\n\nAbstract\nThis is a short intro
duction to linters and their uses.\n\nThe talk assumes some basic familiar
ity with Lean.\n\nI will use the linters in Mathlib as main source of exam
ples.\n\nHowever\, no previous knowledge of linters is required!\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Xavier Généreux and Jannis Limperg (University of Munich (LMU))
DTSTART:20250114T151500Z
DTEND:20250114T154500Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/4
DESCRIPTION:Title: Efficient Forward Reasoning for Aesop\nby Xavier Généreux a
nd Jannis Limperg (University of Munich (LMU)) as part of Lean Together 20
25\n\n\nAbstract\nAesop\, a white-box proof search tactic for Lean\, has l
ong supported forward rules\, which derive additional facts from the hypot
heses in a goal. However\, the initial implementation of this feature did
not scale to local contexts containing many hypotheses. A core limitation
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 though the
local contexts of these goals tend to be very similar.\n\nWe present a new
\, stateful implementation that takes advantage of such similarities to ac
hieve much better performance on various examples. The new implementation
is almost fully backwards compatible and is already Aesop's default. We wi
ll also discuss some ideas for how forward rules can be used to build effe
ctive Aesop rule sets.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Emily Riehl (Johns Hopkins University)
DTSTART:20250114T160000Z
DTEND:20250114T163000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/5
DESCRIPTION:Title: The ∞-cosmos project: formalizing 1-\, 2-\, V-\, and ∞-catego
ry theory in Lean\nby Emily Riehl (Johns Hopkins University) as part o
f Lean Together 2025\n\n\nAbstract\nThe ∞-cosmos project aims to leverag
e the existing libraries developing 1-category theory\, 2-category theory\
, and enriched (V-)category theory in Lean to formalize basic ∞-category
theory. After giving a high-level overview of the problem\, plan\, and pr
ogress of the project (so far)\, we illustrate some challenges related to
the formalization of the supporting results from 1-category theory\, 2-cat
egory theory\, and enriched (V-)category theory that we have encountered t
hus far in hopes of attracting interest from folks who want to help us sol
ve them.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Weber\, Vlad Tsyrklevich
DTSTART:20250114T163000Z
DTEND:20250114T171500Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/6
DESCRIPTION:Title: Equational Theories Project\nby Daniel Weber\, Vlad Tsyrklevi
ch 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\, usin
g Lean to formalize the results. The goal of the project is to classify th
e relationship between all equational theories of magmas in a single equat
ion of up to order 4 (magmas are sets with a closed binary operation with
no additional structure.) The project also has the additional aim of explo
ring new ways of researching mathematics collaboratively. This talk descri
bes some of the aims\, methods\, and results of the project.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lean FRO (Lean FRO)
DTSTART:20250114T173000Z
DTEND:20250114T183000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/7
DESCRIPTION:Title: The Lean FRO Year 2 Roadmap and Vision\nby Lean FRO (Lean FRO
) as part of Lean Together 2025\n\n\nAbstract\nThe Lean Focused Research O
rganization (FRO) envisions a future where Lean becomes a pivotal tool for
driving innovation and progress across diverse fields. Our vision encompa
sses formal mathematics\, software and hardware verification\, software de
velopment\, AI research for mathematics and code synthesis\, as well as ne
w methodologies for math and computer science education. In this talk\, we
will present the Lean FRO's progress to date\, outline our roadmap for Ye
ar 2\, and introduce new team members. We will also explore key initiative
s aimed at enhancing Lean's scalability\, usability\, proof automation\, a
nd documentation.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Renshaw
DTSTART:20250114T183000Z
DTEND:20250114T190000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/8
DESCRIPTION:Title: Searching for Proof Improvements with tryAtEachStep\nby David
Renshaw as part of Lean Together 2025\n\n\nAbstract\nI will present tryAt
EachStep\, a tool that walks through Lean source code and runs a given tac
tic on every proof step. I will discuss how it is implemented\, a variety
of different ways it might be used\, and some results from running it on M
athlib.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Scott Carnahan (University of Tsukuba)
DTSTART:20250115T123000Z
DTEND:20250115T130000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/9
DESCRIPTION:Title: Vertex algebras in Mathlib: coming soon?\nby Scott Carnahan (
University of Tsukuba) as part of Lean Together 2025\n\n\nAbstract\nVertex
algebras appear naturally in the representation theory of Lie algebras an
d finite groups\, but they have a reputation for unwieldy complexity. In o
rder to work with them efficiently\, one typically manipulates formal powe
r series in multiple variables. I will describe some progress toward imple
menting the necessary theory in Mathlib\, and some of the upcoming challen
ges.\n\nThis talk will not assume any knowledge of representation theory o
r Lie algebras.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Siddhartha Gadgil (Indian Institute of Science\, Bangalore)
DTSTART:20250115T130000Z
DTEND:20250115T133000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/10
DESCRIPTION:Title: Real world Autoformalization\nby Siddhartha Gadgil (Indian I
nstitute of Science\, Bangalore) as part of Lean Together 2025\n\n\nAbstra
ct\nAutoformalization shows great promise both in helping formalize mathem
atics and in allowing mathematicians to use the combination of AI and Lean
without expertise in either. We have been working towards realizing this
promise\, focussing on both improving Autoformalization and on tooling and
integration with Lean.\n\nHere I will discuss some of our efforts and tec
hniques that help with autoformalization and with making it usable.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jakob von Raumer (Lindy Labs)
DTSTART:20250115T133000Z
DTEND:20250115T140000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/11
DESCRIPTION:Title: Building a Formal Verification Framework for Smart Contracts
\nby Jakob von Raumer (Lindy Labs) as part of Lean Together 2025\n\n\nAbst
ract\nIn the past two years I have been building a formal verfication tool
called Aegis and used it to verify smart contracts on the Starknet blockc
hain. In my talk I will describe the challenges and the joy of building a
lightweight Lean package that enables a slick verification workflow.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250115T140000Z
DTEND:20250115T143000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/12
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joseph Rotella
DTSTART:20250115T143000Z
DTEND:20250115T150000Z
DTSTAMP:20260428T193228Z
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 wil
l present a Lean library for programming with tabular data. Tables challen
ge many type systems due to their heterogeneity and the need for type-leve
l computations to express many common table operations—challenges to whi
ch Lean's dependent type system is well suited. I will discuss the design\
, implementation\, and verification of this library following the Brown Be
nchmark for Table Types\, a benchmark based on existing tabular programmin
g frameworks.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/13/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Oliver Nash (Google DeepMind)
DTSTART:20250114T141500Z
DTEND:20250114T144500Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/14
DESCRIPTION:Title: Root systems and root data in Mathlib\nby Oliver Nash (Googl
e DeepMind) as part of Lean Together 2025\n\n\nAbstract\nI will discuss th
e formalisation of root systems and root data in Lean's mathematics librar
y\, Mathlib. These structures provide a good example of the idiom that "go
od definitions are hard work". In this case\, part of the challenge is to
have a single definition that simultaneously specialises to root systems\,
root data\, works in any characteristic\, and also permits a theory of in
finite root systems (such as the roots of a Kac-Moody algebra).\n\nThe mat
hematical content will be elementary\, and the emphasis will be on the les
sons for computer formalisation.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250115T153000Z
DTEND:20250115T160000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/15
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Henrik Böving (Lean FRO)
DTSTART:20250115T160000Z
DTEND:20250115T163000Z
DTSTAMP:20260428T193228Z
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 will desc
ribe bv_decide\, a tactic for solving all fixed-width BitVec goals.\nIt wi
ll give an overview of the inner workings of bv_decide as well as a perfor
mance evaluation\, showcasing\nsome applications of bv_decide to real worl
d problems.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lorenzo Luccioli (University of Bologna)
DTSTART:20250115T163000Z
DTEND:20250115T170000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/17
DESCRIPTION:Title: Information theory in Lean: the DPI\nby Lorenzo Luccioli (Un
iversity of Bologna) as part of Lean Together 2025\n\n\nAbstract\nThe Data
Processing Inequality (DPI) is a cornerstone of information theory\, expr
essing the principle that information cannot be created through processing
.\n\nIn this talk\, I will present the formalization of information-theore
tic results carried out by Rémy Degenne and myself using the Lean 4 theor
em prover. The focus will be on the formalization of information divergenc
es—particularly f-divergences—and their associated Data Processing Ine
quality (DPI)\, along with their connection to the framework of hypothesis
testing. I will also discuss the key challenges and design decisions face
d during the project.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Violeta Hernández Palacios (Universidad de Guanajuato)
DTSTART:20250115T170000Z
DTEND:20250115T173000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/18
DESCRIPTION:Title: A Nimble Introduction to Nimbers\nby Violeta Hernández Pala
cios (Universidad de Guanajuato) as part of Lean Together 2025\n\n\nAbstra
ct\nJohn Horton Conway first defined the field of "nimbers" in 1976. This
seemingly innocuous structure arising from the combinatorial game of Nim t
urns out to have surprisingly deep structure\, and nearly five decades lat
er there are still major open problems.\n\nOne of the most surprising resu
lts on nimbers is that they form an algebraically complete field. This tal
k will focus on the mathematics required to arrive at this result and 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 familiarity
with ordinal numbers.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Michael Rothgang (Universität Bonn)
DTSTART:20250116T160000Z
DTEND:20250116T163000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/19
DESCRIPTION:Title: Scaling mathlib: tooling and automation for an ever-growing math
ematics library\nby Michael Rothgang (Universität Bonn) as part of Le
an Together 2025\n\n\nAbstract\nMaintaining the mathlib library in the pre
sence of continuous growth is a challenge in many aspects.\nOn a technical
level\, this relies on a fair amount of custom tooling and automation to
keep things manageable. I will highlight some recent additions in areas su
ch as deprecations\, linting\, bots and a new review dashboard.\nThis invo
lves work by many people\, including Damiano Testa\, Johan Commelin\, Mari
o Carneiro and the author.\n\nThis talk is mostly aimed at mathlib contrib
utors (and reviewers)\, but there will be useful information for mathlib u
sers also.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250116T163000Z
DTEND:20250116T170000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/20
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Floris van Doorn (University of Bonn)
DTSTART:20250116T170000Z
DTEND:20250116T173000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/21
DESCRIPTION:Title: Progress report on the Carleson Project\nby Floris van Doorn
(University of Bonn) as part of Lean Together 2025\n\n\nAbstract\nI will
give a progress report on the Carleson project\, an ongoing formalization
project of a generalization of Carleson's theorem\, a major result in harm
onic analysis.\n\nI will describe the mathematical ideas in the generalize
d results\, the status of the project and some reflections of the collabor
ative nature of the project.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Marcus Rossel
DTSTART:20250116T173000Z
DTEND:20250116T180000Z
DTSTAMP:20260428T193228Z
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 extremely co
mmon proof task supported by efficient and versatile tactics like $\\textt
t{rw}$ and $\\texttt{simp}$. These tactics are\, however\, limiting in tha
t users need to either provide an explicit order and direction of rewrites
\, or rely on a fixed simplification direction. In our talk\, we present a
new (work in progress) tactic for rewriting using equality saturation. Th
is approach allows us to tackle goals which are infeasible for $\\texttt{s
imp}$ without requiring the details needed for $\\texttt{rw}$.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social hour
DTSTART:20250116T180000Z
DTEND:20250116T183000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/23
DESCRIPTION:Title: Gather Town\nby Social hour as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jean-Baptiste Tristan (Amazon)
DTSTART:20250116T183000Z
DTEND:20250116T190000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/24
DESCRIPTION:Title: Verified Foundations for Differential Privacy\nby Jean-Bapti
ste Tristan (Amazon) as part of Lean Together 2025\n\n\nAbstract\nDifferen
tial privacy (DP) has become the gold standard for privacy-preserving data
analysis\, but implementing it correctly has proven challenging. Prior wo
rk has focused on verifying DP at a high level\, assuming the foundations
are correct and a perfect source of randomness is available. However\, the
underlying theory of differential privacy can be very complex and subtle.
Flaws in basic mechanisms and random number generation have been a critic
al source of vulnerabilities in real-world DP systems.\n\nIn this talk\, w
e present SampCert\, the first comprehensive\, mechanized foundation for d
ifferential privacy. SampCert is written in Lean with over 12\,000 lines o
f proof. It offers a generic and extensible notion of DP\, a framework for
constructing and composing DP mechanisms\, and formally verified implemen
tations of Laplace and Gaussian sampling algorithms. SampCert provides (1)
a mechanized foundation for developing the next generation of differentia
lly private algorithms\, and (2) mechanically verified primitives that can
be deployed in production systems. Indeed\, SampCert’s verified algorit
hms power the DP offerings of Amazon Web Services (AWS)\, demonstrating it
s real-world impact.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Abdalrhman Mohamed (Stanford University)
DTSTART:20250116T190000Z
DTEND:20250116T193000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/25
DESCRIPTION:Title: lean-SMT\nby Abdalrhman Mohamed (Stanford University) as par
t of Lean Together 2025\n\n\nAbstract\nIn this talk\, I will present lean-
SMT\, a tactic designed to discharge Lean goals using SMT solvers. The tac
tic translates the negation of a Lean goal into an SMT query and sends it
to cvc5\, a proof-producing SMT solver. If cvc5 determines the query to be
unsatisfiable\, its proof is reconstructed and replayed within Lean.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250116T193000Z
DTEND:20250116T200000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/26
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/26/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jack McKoen (University of Alberta)
DTSTART:20250116T200000Z
DTEND:20250116T203000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/27
DESCRIPTION:Title: Toward functor quasi-categories in Lean\nby Jack McKoen (Uni
versity of Alberta) as part of Lean Together 2025\n\n\nAbstract\nI will di
scuss my ongoing formalization of basic ∞-category theory (adjacent to t
he ∞-cosmos project). In particular\, I have been formalizing a proof th
at the internal hom between quasi-categories is again a quasi-category—a
n important result toward the Yoneda lemma (for example). I will briefly g
o over the proof\, the ingredients that make it work\, and the API I've be
en working on: lifting problems\, weakly saturated classes\, the generatio
n 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:https://researchseminars.org/talk/LeanTogether2025/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Kontorovich (Rutgers University)
DTSTART:20250117T150000Z
DTEND:20250117T153000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/28
DESCRIPTION:Title: Complex Analysis and PrimeNumberTheorem+ in Lean\nby Alex Ko
ntorovich (Rutgers University) as part of Lean Together 2025\n\n\nAbstract
\nWe will report on some experiments with using formalization for large sc
ale collaboration.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Christian Merten (Utrecht University)
DTSTART:20250117T153000Z
DTEND:20250117T160000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/29
DESCRIPTION:Title: Formalizing the Bruhat-Tits tree\nby Christian Merten (Utrec
ht University) as part of Lean Together 2025\n\n\nAbstract\nThe Bruhat-Tit
s tree of $SL_2$ of a local field is an important tool in number theory an
d\na very special case of a Bruhat-Tits building\, which are analogues of
real symmetric spaces in the p-adic world. In this talk\, I will outline i
ts construction in the proof assistant Lean 4 and explain some of the chal
lenges and design decisions that appeared in the process.\n\nThis is joint
work with Judith Ludwig.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250117T160000Z
DTEND:20250117T163000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/30
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hannah Fechtner (Carnegie Mellon University)
DTSTART:20250117T163000Z
DTEND:20250117T170000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/31
DESCRIPTION:Title: Braid Groups in Lean\nby Hannah Fechtner (Carnegie Mellon Un
iversity) as part of Lean Together 2025\n\n\nAbstract\nBraids can be defin
ed topologically (think: intertwined strings in space) or algebraically in
terms of generators and relations. I will discuss the algebraic definitio
n\, and its formalization in Lean. \n\nThe word problem in the braid group
is decidable\, and the larger\, ongoing project is to implement a verifie
d algorithm\, following Dehornoy. I will discuss the formalization of the
first major stage: defining the braid monoid and embedding it into the bra
id group. While formalizing the remaining portion\, I noticed visual intui
tion sneaking into the termination/correctness proof for this algorithm. I
will present a novel pen-and-paper proof which can rescue the claim. \n\n
Lastly\, I will briefly share a peek at a braid visualization widget-to-co
me!\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joseph Tooby-Smith (Reykjavik University)
DTSTART:20250117T170000Z
DTEND:20250117T173000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/32
DESCRIPTION:Title: Physics and Lean\nby Joseph Tooby-Smith (Reykjavik Universit
y) as part of Lean Together 2025\n\n\nAbstract\nThis talk explores the for
malization of physics within Lean. I will present my long-term vision of w
hat such a formalization should look in 10 years and introduce HepLean\, a
project which is a step towards this goal. My aim is give the audience 'f
ood for thought' about the progress being made\, the challenges that lie a
head\, and how the community can contribute to the formalization of physic
s.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/32/
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Kurniadi Angdinata (London School of Geometry and Number The
ory)
DTSTART:20250117T173000Z
DTEND:20250117T180000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/33
DESCRIPTION:Title: Division polynomials of elliptic curves\nby David Kurniadi A
ngdinata (London School of Geometry and Number Theory) as part of Lean Tog
ether 2025\n\n\nAbstract\nElliptic curves are one of the simplest non-triv
ial objects in algebraic geometry and are pervasive in modern number theor
y such as in Wiles's proof of Fermat's last theorem. Their points form an
abelian group under a geometric addition law given by explicit rational fu
nctions. In particular\, there is an explicit formula for the multiplicati
on of a point by $ n $ in terms of certain inductively-defined division po
lynomials\, which are crucial in point counting algorithms and public key
cryptography. In this talk\, I will explain our formalisation of division
polynomials and the multiplication-by-$ n $ formula\, whose proof turned o
ut to be quite elusive. This is joint work with Junyan Xu.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/33/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Yuma Mizuno (University College Dublin)
DTSTART:20250117T180000Z
DTEND:20250117T183000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/34
DESCRIPTION:Title: Metaprogramming on monoidal categories\nby Yuma Mizuno (Univ
ersity 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 monoidal categ
ories or 2-morphisms in bicategories. The coherence tactic is a tactic for
proving coherence conditions within monoidal categories or bicategories.
I will explain how these tools have been implemented using metaprogramming
in Lean.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/34/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leni Aniva (Stanford University Centaur Lab)
DTSTART:20250116T203000Z
DTEND:20250116T210000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/35
DESCRIPTION:Title: Pantograph: A Machine-to-Machine Interaction Interface for Lean
4\nby Leni Aniva (Stanford University Centaur Lab) as part of Lean Tog
ether 2025\n\n\nAbstract\nIn this paper\, we introduce Pantograph\, a tool
that provides a versatile interface to the Lean 4 proof assistant and ena
bles efficient proof search via powerful search algorithms such as Monte C
arlo Tree Search. Pantograph enables high-level reasoning by allowing the
user to control Lean 4's inference steps. We provide an overview of Pantog
raph's architecture and features. We also report on an illustrative use ca
se: using machine learning models and proof sketches to prove Lean 4 theor
ems. Pantograph's innovative features pave the way for more advanced machi
ne learning models to perform complex proof searches and high-level reason
ing\, equipping future researchers to design more versatile and powerful t
heorem provers.\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/35/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250114T154500Z
DTEND:20250114T160000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/36
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/36/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250114T171500Z
DTEND:20250114T173000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/37
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/37/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250114T190000Z
DTEND:20250114T193000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/38
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/38/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Social Time
DTSTART:20250117T183000Z
DTEND:20250117T193000Z
DTSTAMP:20260428T193228Z
UID:LeanTogether2025/39
DESCRIPTION:Title: Gather Town\nby Social Time as part of Lean Together 2025\n\
nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LeanTogether2025/39/
END:VEVENT
END:VCALENDAR