BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CMSA - ECPv6.17.1//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
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:20200308T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20201101T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20210314T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20211107T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20220313T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20221106T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20210303T150000
DTEND;TZID=America/New_York:20210303T160000
DTSTAMP:20240517T194704Z
CREATED:20240126T084416Z
LAST-MODIFIED:20240517T194704Z
UID:10001419-1614783600-1614787200@cmsa.fas.harvard.edu
SUMMARY:Neural Theorem Proving in Lean using Proof Artifact Co-training and Language Models
DESCRIPTION:Speaker: Jason Rute\, CIBO Technologies \nTitle: Neural Theorem Proving in Lean using Proof Artifact Co-training and Language Models \nAbstract: Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built. This is particularly challenging when applying large Transformer language models to tactic prediction\, because the scaling of performance with respect to model size is quickly disrupted in the data-scarce\, easily-overfitted regime. We propose PACT ({\bf P}roof {\bf A}rtifact {\bf C}o-{\bf T}raining)\, a general methodology for extracting abundant self-supervised data from kernel-level proof terms for co-training alongside the usual tactic prediction objective. We apply this methodology to Lean\, an interactive proof assistant which hosts some of the most sophisticated formalized mathematics to date. We instrument Lean with a neural theorem prover driven by a Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32% to 48%.
URL:https://cmsa.fas.harvard.edu/event/3-3-2021-new-tech-in-math/
LOCATION:Virtual
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-New-Technologies-in-Mathematics-03.03.21.png
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20210310T150000
DTEND;TZID=America/New_York:20210310T160000
DTSTAMP:20240517T194750Z
CREATED:20240126T083441Z
LAST-MODIFIED:20240517T194750Z
UID:10001414-1615388400-1615392000@cmsa.fas.harvard.edu
SUMMARY:The Ramanujan Machine: Using Algorithms for the Discovery of Conjectures on Mathematical Constants
DESCRIPTION:Speaker: Ido Kaminer\, Technion – Israel Institute of Technology\, Faculty of Electrical Engineering \nTitle: The Ramanujan Machine: Using Algorithms for the Discovery of Conjectures on Mathematical Constants \nAbstract: In the past\, new conjectures about fundamental constants were discovered sporadically by famous mathematicians such as Newton\, Euler\, Gauss\, and Ramanujan. The talk will present a different approach – a systematic algorithmic approach that discovers new mathematical conjectures on fundamental constants. We call this approach “the Ramanujan Machine”. The algorithms found dozens of well-known formulas as well as previously unknown ones\, such as continued fraction representations of π\, e\, Catalan’s constant\, and values of the Riemann zeta function. Part of the conjectures were in retrospect simple to prove\, whereas others remained so far unproved. We will discuss these puzzles and wider open questions that arose from this algorithmic investigation – specifically\, a newly-discovered algebraic structure that seems to generalize all the known formulas and connect between fundamental constants. We will also discuss two algorithms that proved useful in finding conjectures: a variant of the meet-in-the-middle algorithm and a gradient descent algorithm tailored to the recurrent structure of continued fractions. Both algorithms are based on matching numerical values; consequently\, they conjecture formulas without providing proofs or requiring prior knowledge of the underlying mathematical structure. This way\, our approach reverses the conventional usage of sequential logic in formal proofs; instead\, using numerical data to unveil mathematical structures and provide leads to further mathematical research.
URL:https://cmsa.fas.harvard.edu/event/3-10-2021-new-tech-in-math/
LOCATION:Virtual
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-New-Technologies-in-Mathematics-03.10.21.png
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20210324T150000
DTEND;TZID=America/New_York:20210324T160000
DTSTAMP:20240515T195432Z
CREATED:20240126T083019Z
LAST-MODIFIED:20240515T195432Z
UID:10001411-1616598000-1616601600@cmsa.fas.harvard.edu
SUMMARY:Word and Graph Embeddings for Machine Learning
DESCRIPTION:Speaker: Steve Skiena\, Dept. of Computer Science and AI Insititute\, Stony Brook University \nTitle: Word and Graph Embeddings for Machine Learning \nAbstract: DeepWalk is an approach we have developed to construct vertex embeddings: vector representations of vertices which be applied to a very general class of problems in data mining and information retrieval. DeepWalk exploits an appealing analogy between sentences as sequences of words and random walks as sequences of vertices to transfer deep learning (unsupervised feature learning) techniques from natural language processing to network analysis. It has become extremely popular\, having been cited by over 4600 research papers since its publication at KDD 2014. In this talk\, I will introduce the notion of graph embeddings\, and demonstrate why they make such powerful features for machine learning applications. I will focus on more recent efforts concerning (1) fast embedding methods for very large networks\, (2) techniques for embedding dynamic graphs\, and (3) embedding spaces as models for knowledge generation. \n  \n 
URL:https://cmsa.fas.harvard.edu/event/3-24-2021-new-tech-in-math-seminar/
LOCATION:MA
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-New-Technologies-in-Mathematics-03.24.21.png
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20210331T150000
DTEND;TZID=America/New_York:20210331T160000
DTSTAMP:20240515T195507Z
CREATED:20240126T083143Z
LAST-MODIFIED:20240515T195507Z
UID:10001412-1617202800-1617206400@cmsa.fas.harvard.edu
SUMMARY:Doing Mathematics with Simple Types: Infinitary Combinatorics in Isabelle/HOL
DESCRIPTION:Speaker: Lawrence Paulson\, University of Cambridge Computer Laboratory  \nTitle: Doing Mathematics with Simple Types: Infinitary Combinatorics in Isabelle/HOL  \nAbstract: Are proof assistants relevant to mathematics? One approach to this question is to explore the breadth of mathematical topics that can be formalised. The partition calculus was introduced by Erdös and R. Rado in 1956 as the study of “analogues and extensions of Ramsey’s theorem”. Highly technical results were obtained by Erdös-Milner\, Specker and Larson (among many others) for the particular case of ordinal partition relations\, which is concerned with countable ordinals and order types. Much of this material was formalised last year (with the assistance of Džamonja and Koutsoukou-Argyraki). Some highlights of this work will be presented along with general observations about the formalisation of mathematics\, including ZFC\, in simple type theory. \n\n\n\n\n\n\n\n\n 
URL:https://cmsa.fas.harvard.edu/event/3-31-2021-new-tech-in-math/
LOCATION:MA
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-New-Technologies-in-Mathematics-03.31.21.png
END:VEVENT
END:VCALENDAR