Terence Tao – Machine-Assisted Proofs (February 19, 2025) [video] — https://www.youtube.com/watch?v=5ZIIGLiQWNM
#HackerNews #TerenceTao #MachineAssistedProofs #Mathematics #Video #AIProofs
Terence Tao - Machine-Assisted Proofs (February 19, 2025)

YouTube
CRM Colloquium by Terence Tao: "Machine Assisted Proofs"

YouTube
@djalbat @holbot All the available talks can be found either on the #IPAM youtube channel https://www.youtube.com/channel/UCGzuiiLdQZu9wxDNJHO_JnA or by navigating to the individual talks in the #MachineAssistedProofs workshop web page https://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/?tab=schedule .
Institute for Pure & Applied Mathematics (IPAM)

The Institute for Pure and Applied Mathematics (IPAM) is a National Science Foundation Math Institute at the University of California, Los Angeles (UCLA) that fosters the interaction of mathematics with a broad range of science and technology, builds new interdisciplinary research communities, promotes mathematical innovation, and engages and transforms the world through mathematics. IPAM fulfills its mission through workshops and programs that connect mathematics and other disciplines or multiple areas of mathematics. These activities bring in thousands of visitors annually from academia, government, and industry. The NSF has encouraged IPAM to make the scientific presentations of our speakers available to a wider audience. While this YouTube channel contains many of our most popular videos, our full video archive is available at www.ipam.ucla.edu/videos.

YouTube
@holbot @djalbat This recent #IPAM #MachineAssistedProofs talk by Jason Rute discusses the state of the art in this direction: https://www.youtube.com/watch?v=P5ew0BrRm_I (also discussed here at https://mathstodon.xyz/@tao/109875787762679762 )
Jason Rute - Deep learning in interactive theorem proving - IPAM at UCLA

YouTube
Inspired by the recent #IPAM conference on #MachineAssistedProofs, I wrote a blog post inviting discussion regarding the possibility of automatically generating a logical diagram for a given mathematical paper. https://terrytao.wordpress.com/2023/02/18/would-it-be-possible-to-create-a-tool-to-automatically-diagram-papers/
Hoy culmina el programa de #MachineAssistedProofs , al que le podríamos llamar #MatemáticasAutomáticas . En verdad, hay que pensar que «a todo cerdo le llega su San Martín» y que estamos llegando a un cambio de paradigma, al final de un camino. Poco a poco el trabajo, a veces tedioso y a veces complejo, detrás de una demostración matemática se está automatizando. A penas van los conceptos básicos de algunas áreas, pero ahí va la maquinaria creciendo.
Terence Tao (@[email protected])

The #IPAM workshop on #MachineAssistedProofs (which I am the lead organizer of) starts in less than an hour: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/ . As an experiment, I plan to make some occasional posts on the workshop as comments to this post. (UPDATE: the workshop has now concluded, and videos of the talks are available at https://www.youtube.com/@IPAMUCLA/videos .)

Mathstodon
The #IPAM workshop on #MachineAssistedProofs (which I am the lead organizer of) starts in less than an hour: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/ . As an experiment, I plan to make some occasional posts on the workshop as comments to this post. (UPDATE: the workshop has now concluded, and videos of the talks are available at https://www.youtube.com/@IPAMUCLA/videos .)
Machine Assisted Proofs - IPAM

Machine Assisted Proofs

IPAM