Colloquia

Harold Williams, USC

Monday, February 2nd, 3:30 – 4:30 pm, KAP 414

Title: Automated Theorem Proving in Lean

Abstract: In this talk we give an introduction to Lean, a programming language adapted to the formal verification of mathematical proofs. Lean and its flagship library, mathlib, have been the focus of a dedicated user community for about a decade, but their visibility has grown significantly in light of advances in AI. We will survey some recent developments in AI systems designed to generate proofs in Lean, and in particular compare and contrast two frontier models, Seed-Prover and Aristotle. These were developed by ByteDance and Harmonic, respectively, with the development of the latter being carried out in collaboration with an academic team consisting of myself, Sergei Gukov, Dan Halpern-Leistner, and Alex Meiburg.

_______________________________________________________________________________________________

Sergei Gukov, Caltech

Monday, February 9th, 3:30 – 4:30 pm, KAP 414

Title: TBA

Abstract: TBA

_______________________________________________________________________________________________

Gunnar Carlsson, Stanford University and BluelightAI Inc.

Monday, February 23rd, 3:30 – 4:30 pm, KAP 414

Title: TBA

Abstract: TBA

_______________________________________________________________________________________________

Javier Gomez Serrano, Brown University

Monday, March 2nd, 3:30 – 4:30 pm, KAP 414

Title: TBA

Abstract: TBA

_______________________________________________________________________________________________

Shanghua Teng, USC

Monday, March 9th, 3:30 – 4:30 pm, KAP 414

Title: TBA

Abstract: TBA

_______________________________________________________________________________________________