AI proof discovery and autoformalised libraries

Start Date: October 7, 2026
End Date: October 7, 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): Christopher Birkbeck (University of East Anglia)
Abstract:
AI is helping us prove new theorems and formalise their proofs at an incredible rate, but what do we do with all of this? One option is to contribute the reusable parts to large AI-driven formal libraries such as Tau Ceti. In this talk, I will discuss this process, taking as an example ongoing joint work with Alex Torzewski and ChatGPT Pro on proving and formalising new results about adic spaces.

Events