20 milhões de dólares para um projeto para formalização de matemática, proof assistants, etc.

[samuel]

... Em todos os lugares do Twitter hoje, o coordenador do projeto vai ser o Avigad. 

https://www.cmu.edu/news/stories/archives/2021/september/hoskinson-center-for-formal-mathematics.html

[Walter Carnielli]

Fantástico, certamente Jeremy Avigad tem toda a envergadura para
isso- trabalha simultaneamente com Filosofia e Matemática, e se
alguém pode levar esse "monstro" adiante ele é um deles.

Mas eu pessoalmente acho que há riscos, se a coisa não for feita com
devidas cautelas. Para quem se interessa, escrevi um artigo
recente sobre os risco da Inteligência Artificial na agenda
filosófica:

"How AI can be surprisingly dangerous for the philosophy of
mathematics — and of science" . Circumscribere Vol. 27 (2021)

https://revistas.pucsp.br/index.php/circumhc/article/view/55033

Críticas, contra-argumentos e "dislikes" serão apreciados e considerados :-)

Abs,
Walter



Em qua., 22 de set. de 2021 às 20:51, 'samuel' via LOGICA-L
<logi...@dimap.ufrn.br> escreveu:

>
> ... Em todos os lugares do Twitter hoje, o coordenador do projeto vai ser o Avigad.
>
> https://www.cmu.edu/news/stories/archives/2021/september/hoskinson-center-for-formal-mathematics.html
>

--
===========================
Walter Carnielli, Professor
Centre for Logic, Epistemology and the History of Science and
Department of Philosophy
University of Campinas –UNICAMP
13083-859 Campinas -SP, Brazil
Phone: (+55) (19) 3521-6517
Institutional e-mail: walter.c...@cle.unicamp.br
Website: http://www.cle.unicamp.br/prof/carnielli

[Itala Maria Loffredo D'Ottaviano]

Fantástico!

Ítala

Em qua., 22 de set. de 2021 às 20:51, 'samuel' via LOGICA-L <logi...@dimap.ufrn.br> escreveu:

... Em todos os lugares do Twitter hoje, o coordenador do projeto vai ser o Avigad. 

https://www.cmu.edu/news/stories/archives/2021/september/hoskinson-center-for-formal-mathematics.html

--
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 ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/ec9e09af-181b-4ff3-be62-9a4b4c23470cn%40dimap.ufrn.br.

--

Prof. Dr. Itala M. Loffredo D'Ottaviano

Full Professor in Logic and the Foundations of Science

Centre for Logic, Epistemology and the History of Science

University of Campinas

[Carlos Augusto Prolo]

Eu suspeito que os 20 milhões de dólares sejam basicamente o custo da construção de um novo prédio para abrigar o centro, nem tão grande assim, com alguma mobília, equipamentos, talvez alguma reserva para manutenção por algum tempo.

 Abraço,

Prolo

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGi1dG4DkeTbA5wrp0bH2Q30UXr2CeUYCMArkr3DDHmhNBJNYg%40mail.gmail.com.

[Joao Marcos]

> Eu suspeito que os 20 milhões de dólares sejam basicamente o custo da construção de um novo prédio para abrigar o centro, nem tão grande assim, com alguma mobília, equipamentos, talvez alguma reserva para manutenção por algum tempo.

Aqui neste vídeo (https://youtu.be/3snIzhjqsk0) o próprio Hoskinson
(bilionário dos blockchains) fala sobre o Lean, sobre a importância
das demonstrações matemáticas e sobre algumas das conquistas de
formalização da matemática, e sobre "a interseção entre Computação,
Matemática, Filosofia e Lógica"). Ele também fala sobre a verba que
está doando, que resultará em 1 milhão de dólares por ano, durante um
certo número de anos, e alguma verba adicional para a Carnegie Mellon
construir seu puxadinho, ou gastar como melhor lhe aprouver, neste
projeto. Ele afirma, ainda, que pretende aumentar o investimento
("entre 200 e 250 milhões ao longo da próxima década, ou duas
décadas"), no futuro, para que o Centro se transforme em um Instituto.
Está claro que vai ter bastante verba, em particular, para contratar
pós-doutorandos e estudantes de pós-graduação, e é bom a gente não
subestimar o que o Avigad será capaz de fazer com essa grana. Talvez
a Giselle Reis, que trabalha na CMU e faz parte da nossa comunidade,
tenha mais notícias pra dar pra gente sobre isso?

Sobre puxadinhos, recordo-me de ter ficado surpreso ao descobrir, em
breve passagem por Palo Alto, que a Stanford Encyclopedia of
Philosophy é administrada por um único funcionário que habita uma
única salinha na universidade de Stanford (universidade na qual o
prédio da Computação foi doado por Bill Gates, e o prédio da
Engenharia Elétrica foi doado por David Packard, já que a Microsoft e
a HP ---e a Valeria de Paiva :-D--- estão logo ali do lado).

[]s, Joao Marcos

--
http://sequiturquodlibet.googlepages.com/

[Joao Marcos]

Neste outro vídeo, aparentemente na própria CMU, o Hoskinson (33 anos
de idade) fala um bocado sobre Matemática, fala sobre a ideia de criar
"open-source textbooks" para estudantes (do Ensino Médio em diante, de
qualquer parte do mundo) por meio do Centro que está criando, e fala
também sobre a importância dos Métodos Formais no modelo de negócios
que o deixou rico:
https://youtu.be/gCLJOrJFLZQ
(Devo dizer que uma certa afirmação que ele faz sobre o número de
"practicing mathematicians" na África me soa incorreta.)

%%%

Agora, vou também
"dar uma queixadinha
Porque eu sou um rapaz latino-americano
Que também sabe se lamentar":

Infelizmente, por falta de visão e estratégia, a minha universidade (e
o meu departamento, que não foi capaz de acolhê-lo enquanto ele esteve
dando sopa por aqui) acabou de _perder_ aquele que é possivelmente o
maior especialista nacional na área de Métodos Formais... E não foi a
nossa única perda...

Enquanto isso, a grande inteligência brasileira (e da UFRN) está agora
com a convicção de que vai se tornar _grande potência na área de IA_
(de onde a inteligência vai tirar os profissionais que ele não forma
nem é capaz de atrair ou manter, eu não sei).
https://www.gov.br/mcti/pt-br/acompanhe-o-mcti/transformacaodigital/inteligencia-artificial
Pelo que pude acompanhar, tivemos um concurso em julho para esta área
no IMD/UFRN e ninguém foi aprovado, e abrimos depois disso abrimos no
DIMAp/UFRN um edital de remoção também para esta área e não tivemos
sequer candidatos?

%%%

[]s, JM


JM