#MachineAssistedProofs

0 posts0 participants0 posts today

Hacker NewsTerence Tao – Machine-Assisted Proofs (February 19, 2025) [video] — <a href="https://www.youtube.com/watch?v=5ZIIGLiQWNM" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.youtube.com/watch?v=5ZIIGLiQWNM</a> <a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HackerNews</a> <a href="https://mastodon.social/tags/TerenceTao" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TerenceTao</a> <a href="https://mastodon.social/tags/MachineAssistedProofs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#MachineAssistedProofs</a> <a href="https://mastodon.social/tags/Mathematics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Mathematics</a> <a href="https://mastodon.social/tags/Video" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Video</a> <a href="https://mastodon.social/tags/AIProofs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AIProofs</a>

guIA - guía a la IA<a href="https://www.youtube.com/watch?v=U1lxSSTbf9k" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.youtube.com/watch?v=U1lxSSTbf9k</a> <a href="https://sigmoid.social/tags/mathematics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#mathematics</a> <a href="https://sigmoid.social/tags/machineassistedproofs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#machineassistedproofs</a>

Terence Tao<a href="https://mathstodon.xyz/@djalbat" class="u-url mention">@djalbat</a> <a href="https://mas.to/@holbot" class="u-url mention">@holbot</a> All the available talks can be found either on the <a href="https://mathstodon.xyz/tags/IPAM" class="mention hashtag" rel="tag">#IPAM</a> youtube channel <a href="https://www.youtube.com/channel/UCGzuiiLdQZu9wxDNJHO_JnA" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.youtube.com/channel/UCGzuiiLdQZu9wxDNJHO_JnA</a> or by navigating to the individual talks in the <a href="https://mathstodon.xyz/tags/MachineAssistedProofs" class="mention hashtag" rel="tag">#MachineAssistedProofs</a> workshop web page <a href="https://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/?tab=schedule" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/?tab=schedule</a> .

Terence Tao<a href="https://mas.to/@holbot" class="u-url mention">@holbot</a> <a href="https://mathstodon.xyz/@djalbat" class="u-url mention">@djalbat</a> This recent <a href="https://mathstodon.xyz/tags/IPAM" class="mention hashtag" rel="tag">#IPAM</a> <a href="https://mathstodon.xyz/tags/MachineAssistedProofs" class="mention hashtag" rel="tag">#MachineAssistedProofs</a> talk by Jason Rute discusses the state of the art in this direction: <a href="https://www.youtube.com/watch?v=P5ew0BrRm_I" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.youtube.com/watch?v=P5ew0BrRm_I</a> (also discussed here at <a href="https://mathstodon.xyz/@tao/109875787762679762" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://mathstodon.xyz/@tao/109875787762679762</a> )

Terence TaoInspired by the recent <a href="https://mathstodon.xyz/tags/IPAM" class="mention hashtag" rel="tag">#IPAM</a> conference on <a href="https://mathstodon.xyz/tags/MachineAssistedProofs" class="mention hashtag" rel="tag">#MachineAssistedProofs</a>, I wrote a blog post inviting discussion regarding the possibility of automatically generating a logical diagram for a given mathematical paper. <a href="https://terrytao.wordpress.com/2023/02/18/would-it-be-possible-to-create-a-tool-to-automatically-diagram-papers/" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://terrytao.wordpress.com/2023/02/18/would-it-be-possible-to-create-a-tool-to-automatically-diagram-papers/</a>

pablo suárez-serratoHoy culmina el programa de <a href="https://fediunam.site/tags/MachineAssistedProofs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#MachineAssistedProofs</a> , al que le podríamos llamar <a href="https://fediunam.site/tags/Matem%C3%A1ticasAutom%C3%A1ticas" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#MatemáticasAutomáticas</a> . 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.

Applied Geometry LabML4PureMath in the <a href="https://sigmoid.social/tags/MachineAssistedProofs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#MachineAssistedProofs</a> workshop at <a href="https://sigmoid.social/tags/IPAM" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IPAM</a> this week. <a href="https://mathstodon.xyz/@tao/109858184238417737" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/@tao/109858184238417737</a>

pablo suárez-serratoEsta semana estaré participando en <a href="https://fediunam.site/tags/IPAM" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IPAM</a> en <a href="https://fediunam.site/tags/UCLA" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#UCLA</a> en un programa de <a href="https://fediunam.site/tags/MachineAssistedProofs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#MachineAssistedProofs</a> . Se tratará la automatización de demostraciones matemáticas. Mi primera experiencia con esto fue cuando en 2015 demostramos, con Luis García-Naranjo y Ramón Vera, que toda 4-variedad lisa admite una estructura de Poisson. Para la prueba tuvimos que apoyarnos en calculos que realizamos con un programa en Mathematica, de cómputo simbólico. <a href="https://link.springer.com/article/10.1007/s11005-015-0792-8" rel="nofollow noopener noreferrer" target="_blank">https://link.springer.com/article/10.1007/s11005-015-0792-8</a>

Terence TaoThe <a href="https://mathstodon.xyz/tags/IPAM" class="mention hashtag" rel="tag">#IPAM</a> workshop on <a href="https://mathstodon.xyz/tags/MachineAssistedProofs" class="mention hashtag" rel="tag">#MachineAssistedProofs</a> (which I am the lead organizer of) starts in less than an hour: <a href="http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/" target="_blank" rel="nofollow noopener noreferrer" translate="no">http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/</a> . 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 <a href="https://www.youtube.com/@IPAMUCLA/videos" target="_blank" rel="nofollow noopener noreferrer" translate="no">https://www.youtube.com/@IPAMUCLA/videos</a> .)

Recent searches

Search options

Administered by:

Server stats:

#MachineAssistedProofs