Menos de um mês depois, a tarefa de formalização em Lean já foi concluída:
https://twitter.com/AlexKontorovich/status/1731692984771428633

JM

On Wed, Nov 15, 2023 at 8:25 PM Joao Marcos <[email protected]> wrote:
>
> E por falar em Lean, os interessados em matemática formalizada
> provavelmente irão querer ficar de olho neste projeto recente do
> Terence Tao (com Tim Gowers, Ben Green, Freddie Manners):
> https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/
> https://mathstodon.xyz/@tao/111404473592619929
> https://teorth.github.io/pfr/blueprint/dep_graph_document.html
>
> []s, JM
>
> On Tue, Nov 14, 2023 at 9:49 AM Adolfo Neto <[email protected]> wrote:
> >
> >
> > Neste episódio do Fronteiras da Engenharia de Software, Adolfo Neto 
> > entrevista o pesquisador Leonardo de Moura, Senior Principal Applied 
> > Scientist no Grupo de Raciocínio Automatizado na AWS e Chief Architect da 
> > Lean FRO. Leonardo é reconhecido por diversas contribuições, entre elas o 
> > desenvolvimento do Z3, um SMT Solver, e da Lean, que é ao mesmo tempo uma 
> > linguagem de programação funcional e um provador de teoremas.
> >
> > https://fronteirases.github.io/episodios/paginas/41
> >
> >
> > --
> > ==================================================================
> > Adolfo Neto
> > Associate Professor - Federal University of Technology, Paraná
> > Web: http://www.dainf.ct.utfpr.edu.br/~adolfo
> > Mestrado em Computação Aplicada: http://www.ppgca.ct.utfpr.edu.br
> > ==================================================================
> >
> > --
> > LOGICA-L
> > Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 
> > <[email protected]>
> > ---
> > 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 [email protected].
> > Para acessar essa discussão na Web, acesse 
> > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANspyYUguAdej_2KY66CAD3-ON7op2SpUZiw7Mudn5i3d0vNrw%40mail.gmail.com.
>
>
>
> --
> http://sequiturquodlibet.googlepages.com/



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

-- 
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica 
<[email protected]>
--- 
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 [email protected].
Para acessar esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LhjKKnW5anwHTPhRy5B6mPPxjDisVAuK%2BkwwePHKEFmRQ%40mail.gmail.com.

Responder a