(Fun)damental Uses of AI in Math:Formalization and Autoformalization
Columbia researchers Alex Kontorovich and Henry Yuen discuss how AI and automated reasoning are changing the formalization of mathematical arguments, including autoformalization of informal proofs. The talk at Schapiro CEPSR's Davis Auditorium (Room 412) covers key challenges and recent progress at the intersection of AI and math.