AI Will Become Mathematicians’ ‘Co-Pilot’

[Joao Marcos]

AI Will Become Mathematicians’ ‘Co-Pilot’
- Fields Medalist Terence Tao explains how proof checkers and AI
programs are dramatically changing mathematics
https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/

(incluindo grande propaganda do LEAN)


JM

[Thiago Nascimento da Silva]

Bem interessante a matéria. Eu tenho acompanhado algumas discussões no fórum do LEAN e inclusive participei de algumas reuniões para ver se tinha algo que eu conseguia pegar para implementar. Sempre vejo comentários sobre novas teorias que foram implementadas para a biblioteca deles.

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lirt0Tmokp3bqzEoeYTv%3Df7TF3LJPZPAdQ2uudUvk-5cw%40mail.gmail.com.

[Marcelo Finger]

O problema é que essa passagem para o uso de provadores de teoremas baseados em IA traz junto todos os problemas de IA que outras áreas já enfrentam.

Muitos matemáticos terão que ser retreinados, e muitíssimo se recusarão a sê-lo. Isso terá como consequência possível um decréscimo no número de matemáticos praticantes.  Enfim, algo que já vem ocorrendo nas áreas do direito, da música, do design e da publicidade.  

Mas é importante frisar que a parte crucial, que é imaginar a estratégia de prova, não foi automatizada (ainda).

[]s

Em seg., 10 de jun. de 2024 às 09:11, Joao Marcos <boto...@gmail.com> escreveu:

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lirt0Tmokp3bqzEoeYTv%3Df7TF3LJPZPAdQ2uudUvk-5cw%40mail.gmail.com.

--

Marcelo Finger
 Departament of Computer Science, IME-USP   
 http://www.ime.usp.br/~mfinger

 ORCID: https://orcid.org/0000-0002-1391-1175
 ResearcherID: A-4670-2009

Instituto de Matemática e Estatística,

Universidade de São Paulo

Rua do Matão, 1010 - CEP 05508-090 - São Paulo, SP

[Joao Marcos]

> Muitos matemáticos terão que ser retreinados, e muitíssimo se recusarão a sê-lo.

Ah, pois, isso me faz lembrar de como o Instituto Metrópole Digital da
UFRN conseguiu contratar, há poucos anos, servidores "especialistas em
editoração eletrônica" que se recusam a aprender a usar LaTeX...

[]s, Joao Marcos

--
https://sites.google.com/site/sequiturquodlibet/

[Alexandre Rademaker]

Exato. E o mesmo vale para programação. E o Lean ajuda a mostrar como estas duas tarefas são a mesma.

—-
Alexandre Rademaker
http://arademaker.github.io

[Carlos Augusto Prolo]

Mas olhando um pouco mais para trás ainda, em áreas de processamento cognitivo em que a inserção da IA ocorreu a mais tempo, parece que deu certo. Os casos óbvios que me vem à mente são os da [assistência] à tradução de textos e correção/aconselhamento ortográfico/gramatical.

Abraço,

Prolo

Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.

Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.

Para acessar essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGG7Aw0OMXcGZ62NVJW7c2GcwFGOX%2BhiM5aYO9KL-V-52S7CQw%40mail.gmail.com.