BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Gabriel Poesia (Harvard University) DTSTART:20251106T190000Z DTEND:20251106T200000Z DTSTAMP:20260423T035958Z UID:OLS/181 DESCRIPTION:Title: Le arning formal mathematical abstractions\nby Gabriel Poesia (Harvard Un iversity) as part of Online logic seminar\n\n\nAbstract\nMathematical abst ractions are devices that enable general representations of many concrete mathematical objects at once: they include definitions\, lemmas\, proof st rategies and algorithms. Typically\, computer agents applied in formal mat hematics are given a set of human-created abstractions (e.g.\, definitions \, tactics\, lemmas in Lean's mathematical library) and receive tasks that involve using and combining those (e.g.\, proving a given theorem). This talk will instead focus on our work on automatically learning the abstract ions themselves. We'll first describe our initial work on this line on lea rning problem-solving tactics for Khan Academy algebra problems in a simpl e dependently-typed theorem proving environment. Then\, we will use these principles to learn tactics in the Rocq (formerly Coq) theorem prover from existing corpora of human proofs. In both cases\, tactic learning is oper ationalized by a symbolic compression procedure\, a principle that has bee n fruitful in learning abstractions in the field of program synthesis. I'l l end by briefly describing ongoing work on a compression-based library le arning method for terms in Lean's type theory\, and highlight several appl ications of this tool. In particular\, compressing sets of theorem stateme nts yields new mathematical definitions that help compactly rewrite the st atements\, whereas compressing proof terms gives rise to lemmas that short en existing proofs.\n LOCATION:https://researchseminars.org/talk/OLS/181/ END:VEVENT END:VCALENDAR