Recorded 15 February 2023. Tony Wu of Google presents "Autoformalization with Large Language Models" at IPAM's Machine Assisted Proofs Workshop. Abstract: Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. While the long-term goal of autoformalization seemed elusive for a long time, we show large language models provide new prospects towards this goal. Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/