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
On
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
> On 10 Jun 2024, at 10:57, Marcelo Finger wrote:
>
> Mas é importante frisar que a parte crucial, que é imaginar a estratégia de
>
> 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...
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
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.
Em seg., 10
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
--
LOGICA-L
