BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CMSA - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:CMSA
X-ORIGINAL-URL:https://cmsa.fas.harvard.edu
X-WR-CALDESC:Events for CMSA
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/New_York
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20220313T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20221106T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20230312T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20231105T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20240310T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20241103T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20231011T140000
DTEND;TZID=America/New_York:20231011T150000
DTSTAMP:20260423T015633
CREATED:20240223T114336Z
LAST-MODIFIED:20240223T114336Z
UID:10002868-1697032800-1697036400@cmsa.fas.harvard.edu
SUMMARY:LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
DESCRIPTION:New Technologies in Mathematics Seminar \nSpeaker: Alex Gu\, MIT Dept. of EE&CS \nTitle: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models \nAbstract: Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However\, existing methods are difficult to reproduce or build on\, due to private code\, data\, and large compute requirements. This has created substantial barriers to research on machine learning methods for theorem proving. We introduce LeanDojo: an open-source Lean playground consisting of toolkits\, data\, models\, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs\, providing valuable data for premise selection: a key bottleneck in theorem proving. Using this data\, we develop ReProver (Retrieval-Augmented Prover): the first LLM-based prover that is augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo’s program analysis capability to identify accessible premises and hard negative examples\, which makes retrieval much more effective. Furthermore\, we construct a new benchmark consisting of 96\,962 theorems and proofs extracted from Lean’s math library. It features a challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation\, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research. \n 
URL:https://cmsa.fas.harvard.edu/event/nt-101123-2/
LOCATION:CMSA Room G10\, CMSA\, 20 Garden Street\, Cambridge\, MA\, 02138\, United States
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-NTM-Seminar-10.11.2023.png
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20231011T163000
DTEND;TZID=America/New_York:20231011T180000
DTSTAMP:20260423T015633
CREATED:20240222T060902Z
LAST-MODIFIED:20240222T060902Z
UID:10002785-1697041800-1697047200@cmsa.fas.harvard.edu
SUMMARY:Non-invertible symmetries\, leptons\, quarks\, and why multiple generations
DESCRIPTION:Quantum Matter Seminar \nSpeaker: Seth Koren (Notre Dame) \nTitle: Non-invertible symmetries\, leptons\, quarks\, and why multiple generations \nAbstract: Generalized global symmetries are present in theories of particle physics\, and understanding their structure can give insight into these theories and UV completions thereof.  After discussing the generalized symmetries of the Standard Model\, we will go Beyond and show that the identification of a non-invertible symmetry of Z’ models of L_µ – L_τ reveals the existence of non-Abelian horizontal gauge theories which naturally produce exponentially small Dirac neutrino masses. Next we will uncover a subtler non-invertible symmetry in horizontal gauge theories of the quark sector which will lead us to a massless down-type quarks solution to strong CP in color-flavor unification. Intriguingly\, this theory works by virtue of the SM having the same numbers of colors and generations.
URL:https://cmsa.fas.harvard.edu/event/qm_101123/
LOCATION:CMSA Room G10\, CMSA\, 20 Garden Street\, Cambridge\, MA\, 02138\, United States
CATEGORIES:Quantum Matter
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-QMMP-10.11.23.png
END:VEVENT
END:VCALENDAR