Re: [Logica-l] 20 milhões de dólares para um projeto para formalização de matemática, proof assistants, etc.

2021-09-22 Por tôpico 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

-- 
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+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LiEpKPtCkeSfANZfOCsc76Yr8wHDnXB58u2t8T4%2Bao2Cw%40mail.gmail.com.

Re: [Logica-l] 20 milhões de dólares para um projeto para formalização de matemática, proof assistants, etc.

2021-09-22 Por tôpico 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/

-- 
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+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LhdXQbh91u6oABixmJnWjW8HtZ8-CHNDsfH__Hxtj0Y1g%40mail.gmail.com.

Re: [Logica-l] 20 milhões de dólares para um projeto para formalização de matemática, proof assistants, etc.

2021-09-22 Por tôpico 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



On Wed, Sep 22, 2021 at 9:38 PM Itala Maria Loffredo D'Ottaviano <
it...@unicamp.br> wrote:

> Fantástico!
> Ítala
>
> Em qua., 22 de set. de 2021 às 20:51, 'samuel' via LOGICA-L <
> logica-l@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+unsubscr...@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
>
> --
> 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+unsubscr...@dimap.ufrn.br.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGi1dG4DkeTbA5wrp0bH2Q30UXr2CeUYCMArkr3DDHmhNBJNYg%40mail.gmail.com
> 
> .
>

-- 
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+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAD7MeJvKg-OCDBc5Nv1R1-2R3-X1zM4TA8skgQGenP0LVPnCEw%40mail.gmail.com.

Re: [Logica-l] 20 milhões de dólares para um projeto para formalização de matemática, proof assistants, etc.

2021-09-22 Por tôpico Itala Maria Loffredo D'Ottaviano 
Fantástico!
Ítala

Em qua., 22 de set. de 2021 às 20:51, 'samuel' via LOGICA-L <
logica-l@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+unsubscr...@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

-- 
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+unsubscr...@dimap.ufrn.br.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGi1dG4DkeTbA5wrp0bH2Q30UXr2CeUYCMArkr3DDHmhNBJNYg%40mail.gmail.com.

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

2021-09-22 Por tôpico 'samuel' via LOGICA-L 
... 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ê 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+unsubscr...@dimap.ufrn.br.
Para ver esta 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.