Para informação! Segue convite de palestra nesta quinta-feira as 16h. https://ide-fgv-br.zoom.us/meeting/register/tJ0rd-qoqjkqG9Em6l3_Mo75CENtWp9PfuBX <https://ide-fgv-br.zoom.us/meeting/register/tJ0rd-qoqjkqG9Em6l3_Mo75CENtWp9PfuBX>
Ab., Alexandre > Subject: Seminário 5/11/2020 - Kevin Buzzard > Date: 2 November 2020 11:24:45 GMT-3 > Cc: Alexandre Rademaker <[email protected]> > > Titulo: Teaching mathematics to computers. > > Palestrante: Kevin Buzzard > > Resumo: > Computers have changed the way that mathematics is done. The ability to do > complicated calculations quickly has enabled humans to numerically solve > differential equations, to check conjectures in number theory in billions of > cases, and many many other examples. In applied mathematics in particular, > the computer has revolutionised the subject. > But there are some areas of pure mathematics where computers are essentially > completely unused. People studying theoretical questions about > infinite-dimensional objects might find that traditional uses of computers > are of no help to them -- they are trying to prove theorems, not compute > examples. > Computer proof verification software offers a new way of using computers, > which might be more useful to mathematicians looking for proofs. I will > demonstrate some of this software (the Lean theorem prover, being developed > by Microsoft Research), talk about why most mathematicians don't use it, and > speculate about whether this will change in the future. No advanced pure > mathematics background will be necessary. > > Mini CV: > Kevin Buzzard is a professor of pure mathematics at Imperial College London. > He was a PhD student of Richard Taylor and his traditional mathematical work > is in algebraic number theory. More recently he has become interested in > teaching modern mathematical proofs to computers. > > Convite: > > Inscreva-se antecipadamente para esta reunião: > https://ide-fgv-br.zoom.us/meeting/register/tJ0rd-qoqjkqG9Em6l3_Mo75CENtWp9PfuBX > > <https://ide-fgv-br.zoom.us/meeting/register/tJ0rd-qoqjkqG9Em6l3_Mo75CENtWp9PfuBX> > > Após a inscrição, você receberá um e-mail de confirmação contendo informações > sobre como entrar na reunião. -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/9385933B-A868-4C20-8E17-DCB978420CF1%40gmail.com.
