Adventures in Autoformalization (and what's next)

Start Date: October 14, 2026
End Date: October 14, 2026
Event Start Time: 10:00 AM
Event End Time: 11:00 AM
Seminar Type: Current Seminars
Seminar location:
Hill Center | Room 705
Rutgers University | Busch Campus | Piscataway, NJ

Also available on Zoom: https://rutgers.zoom.us/j/94999749212?pwd=mBADyoubpVrIexy6X34S6nj47ft316.1
Passcode: 516100
Seminar Series: AI and Mathematics Seminar
Presenter(s): Wesley Pegden, CMU
Abstract:
I'll talk about autoformalization with "Trellis", a system I've built to autonomously formalize math papers into lean with LLM agents; TeX in, Lean out. I'll talk about how it works and what you can use it for. If time permits, I'll discuss some thoughts on the broader impact of LLM agents (and Lean) on our world of mathematics.

Events