T06E41 O Teorema das Quatro Cores
Resumo
O episódio explora o Teorema das Quatro Cores, um problema matemático que afirma que qualquer mapa planar pode ser colorido com apenas quatro cores sem que regiões adjacentes compartilhem a mesma cor. A convidada Gisele Seco, professora de filosofia, explica a formulação simples do problema, sua origem histórica em 1854 com um professor de geografia, e as condições necessárias para sua validade (mapas planares, normais e minimais).
A discussão avança para a história da demonstração do teorema, destacando como ele permaneceu como conjectura por décadas até ser provado em 1976 por Kenneth Appel e Wolfgang Haken usando computadores. Esta foi a primeira prova matemática significativa que dependeu essencialmente de assistência computacional, exigindo mais de 1.200 horas de processamento para verificar 1.498 configurações inevitáveis através de métodos combinatórios.
O programa aborda as controvérsias filosóficas geradas por esta demonstração, particularmente o debate sobre se ela constituía uma verdadeira prova matemática ou um experimento computacional. Gisele discute as reações divididas na comunidade matemática - entre os mais jovens fascinados e os mais velhos céticos - e como este caso abriu discussões sobre a natureza da prova matemática e o papel dos computadores na matemática.
Finalmente, a conversa explora as implicações contemporâneas, incluindo o surgimento da ‘matemática experimental’ e como o Teorema das Quatro Cores continua sendo um caso de estudo importante para filósofos interessados em demarcação do conhecimento, filosofia da computação e análise das práticas matemáticas atuais que incorporam ferramentas computacionais.
Indicações
Conceitos
- Filosofia da Prática Matemática — Abordagem filosófica que foca em descrever o que os matemáticos realmente fazem em sua prática, em contraste com a filosofia fundacionalista que se preocupa com os fundamentos lógicos ou intuitivos da matemática.
- Provas Assistidas por Computador — Área da matemática que utiliza computadores não apenas como ferramentas de cálculo, mas como participantes ativos na construção e verificação de demonstrações matemáticas, como no caso do Teorema das Quatro Cores.
Pessoas
- Augustus De Morgan — Matemático britânico a quem foi apresentado o problema original do Teorema das Quatro Cores pelo irmão de um professor de geografia, e que deu uma formulação mais precisa ao problema.
- Kenneth Appel e Wolfgang Haken — Matemáticos que em 1976 provaram o Teorema das Quatro Cores usando computadores, verificando 1.498 configurações inevitáveis - a primeira prova matemática significativa dependente de assistência computacional.
- Thomas Tymoczko — Filósofo que em 1979 publicou artigo influente argumentando que a prova do Teorema das Quatro Cores representava um ‘híbrido entre prova e experimento’, iniciando debate filosófico sobre o papel dos computadores na matemática.
Linha do Tempo
- 00:00:00 — Introdução ao programa e apresentação do tema — Apresentação do programa Fronteiras da Ciência e da convidada Gisele Seco, professora de filosofia. Marco de Arte introduz o tema aparentemente matemático do Teorema das Quatro Cores e questiona por que uma filósofa estaria interessada neste problema. Gisele começa explicando a formulação intuitiva do teorema: qualquer mapa pode ser colorido com apenas quatro cores sem que regiões adjacentes compartilhem a mesma cor.
- 00:03:05 — Condições e limitações do teorema — Discussão sobre as condições necessárias para o teorema valer: mapas devem ser planares, normais e minimais. Explicação do que significa ‘adjacente’ (compartilhamento de lado com comprimento não nulo, não apenas pontos). Exemplos como tabuleiro de xadrez (duas cores) e fatia de pizza (duas cores). Definição de mapa normal: não pode ter regiões isoladas (como Fernando de Noronha no mapa do Brasil) ou regiões bifurcadas.
- 00:06:19 — História da demonstração e uso de computadores — Gisele explica que o interesse filosófico no teorema surge do modo como foi demonstrado. A primeira pretensa prova foi em 1879, mas continha erros. A prova aceita surgiu em 1976 por Appel e Haken, dependendo essencialmente de computadores. Ela destaca que um ser humano não conseguiria realizar a prova no tempo de uma vida devido à quantidade de casos (1.498 configurações) que precisavam ser verificados por exaustão.
- 00:09:06 — Estratégia da prova e papel do computador — Explicação detalhada da estratégia da prova: assume-se por contradição que existe um mapa que requer cinco cores (pentacromático minimal), então mostra-se que todo mapa contém pelo menos uma configuração de um conjunto inevitável que é redutível (pode ser colorida com quatro cores). O computador foi usado para construir este conjunto inevitável e verificar a redutibilidade de cada configuração através de métodos combinatórios, transformando o problema de colorir mapas em um problema de combinatória.
- 00:16:49 — Implicações filosóficas da prova computacional — Discussão sobre por que esta prova é interessante para filósofos da matemática: representa a primeira prova matemática significativa que não é humanamente produzível nem verificável do início ao fim. Gisele menciona o artigo de Thomas Tymoczko (1979) que caracterizou a prova como um ‘híbrido entre prova e experimento’. Debate sobre se isso introduz experimentação na matemática, tradicionalmente vista como campo do conhecimento a priori.
- 00:22:37 — Reações da comunidade matemática e filosófica — Descrição das reações quando a prova foi apresentada: matemáticos mais jovens ficaram fascinados, enquanto os mais velhos questionavam como confiar em uma prova produzida por computador. Comparação com o Último Teorema de Fermat, onde testes computacionais aumentavam a confiança mas não constituíam prova. Discussão sobre como atitudes mudaram desde então, com a área de demonstrações assistidas por computador sendo mais aceita hoje, embora o Teorema das Quatro Cores permaneça como curiosidade histórica e caso de estudo filosófico.
- 00:27:34 — Filosofia da prática matemática contemporânea — Discussão sobre a filosofia da prática matemática versus filosofia fundacionalista da matemática. Enquanto os fundacionalistas (como Frege, Hilbert, Brouwer) preocupavam-se com os fundamentos da matemática, os filósofos da prática matemática focam em descrever o que os matemáticos realmente fazem. Se matemáticos incorporam computadores em seu trabalho, cabe aos filósofos analisar esses usos. O caso do Teorema das Quatro Cores abre investigações interessantes sobre filosofia da computação.
- 00:31:18 — Aspecto retórico e social das demonstrações — Discussão sobre o aspecto retórico das demonstrações matemáticas: como a explicação varia dependendo do público (especialistas, alunos, leigos). No caso da prova computacional, surge uma nova entidade - o computador - que ‘sabe’ a prova de uma forma que o matemático não pode seguir passo a passo. Debate sobre o que significa ‘verificar’ uma prova e a distinção entre verificabilidade algorítmica (que humanos não podem fazer sozinhos) e sinopticidade (ter uma visão geral do procedimento).
- 00:36:08 — Outros teoremas com provas assistidas por computador — Pergunta sobre se o Teorema das Quatro Cores foi o único caso de prova assistida por computador. Gisele menciona que desde a década de 1950 já havia provas mecanizadas de teoremas lógico-matemáticos (como os 38 primeiros teoremas do Principia Mathematica), mas esses eram teoremas já provados. A singularidade do Teorema das Quatro Cores é que foi o primeiro teorema não resolvido cuja primeira solução foi gerada por computador. Ela cita um volume especial da Notices of the American Mathematical Society (2008) com lista de resultados similares.
Dados do Episódio
- Podcast: Fronteiras da Ciência
- Autor: Fronteiras da Ciência/IF-UFRGS
- Categoria: Science
- Publicado: 2015-12-07T13:00:00Z
Referências
- URL PocketCasts: https://pocketcasts.com/podcast/fronteiras-da-ci%C3%AAncia/fb4669d0-4a98-012e-1aa8-00163e1b201c/t06e41-o-teorema-das-quatro-cores/4cc19e70-7f72-0133-2d47-6dc413d6d41d
- UUID Episódio: 4cc19e70-7f72-0133-2d47-6dc413d6d41d
Dados do Podcast
- Nome: Fronteiras da Ciência
- Site: http://frontdaciencia.ufrgs.br
- UUID: fb4669d0-4a98-012e-1aa8-00163e1b201c
Transcrição
[00:00:00] Este é o programa Fronteiras da Ciência, da rádio da Universidade, onde discutiremos
[00:00:10] os limites entre o que é ciência e o que é mito.
[00:00:14] O convidado do programa de hoje é a Gisele Seco, que é professora aqui do Departamento
[00:00:18] de Filosofia da URX.
[00:00:20] O assunto do programa de hoje é uma coisa esquisita, na minha opinião, para uma filósofa,
[00:00:24] que é um problema que eu caracterizaria como de matemática, mas aí ela vai me mostrar
[00:00:28] errado até o final do programa, espere aí.
[00:00:31] E o pessoal aqui do programa hoje vai ser eu, Marco de Arte, e o Jéfer Sorenson do
[00:00:36] Departamento de Física da URX.
[00:00:38] Então eu vou passar já a palavra rapidamente para a Gisele.
[00:00:41] Por que uma filósofa estuda um teorema sobre cores?
[00:00:44] Então primeiro, eu acho que vamos começar assim, tu explica o que é o teorema.
[00:00:47] Todo mundo já ouviu falar mais ou menos o problema, mas é bom a gente definir ele
[00:00:51] bem direitinho.
[00:00:52] Então, antes de responder, por que alguém da filosofia se interessaria por um teorema
[00:00:56] matemático, especificamente o Teorema das Quatro Cores, é bem verdade que ele é relativamente
[00:01:02] conhecido na comunidade matemática e mesmo fora dela, na medida em que ele é um problema
[00:01:07] simples de ser compreendido na sua formulação primeira, até uma criança pode entender o
[00:01:12] problema.
[00:01:13] Se todo o mapa pode ser colorido só com quatro cores, sem que nenhuma região adjacente seja
[00:01:18] colorida com a mesma cor, essa seria, digamos, a formulação intuitiva, a formulação em
[00:01:22] linguagem comum do problema.
[00:01:24] E de fato foi assim que ele foi formulado pela primeira vez, em 1854, se não me engano,
[00:01:30] por um professor de geografia que estava de fato coloriendo mapas.
[00:01:33] E a dúvida surgiu.
[00:01:35] O irmão desse professor de geografia era matemático e aluno do Augustus de Morgan,
[00:01:40] e foi esse irmão da pessoa que pensou no problema, foi quem foi responsável por introduzir
[00:01:45] na comunidade matemática, que por sua vez deu uma formulação mais precisa e matemática
[00:01:50] para o problema.
[00:01:51] Porque eu acho que as pessoas pensam assim, ah, em geral o mapa tem muitas cores diferentes.
[00:01:55] Porque a gente vê um mapa, um mundo, assim, ele tem diversas cores.
[00:01:58] Mas a questão é que só com quatro cores você já conseguiria pintar ele direitinho.
[00:02:02] Tanto que os mapas reais, como eles não são coloridos com um número mínimo de cores,
[00:02:08] esse problema não aparece na literatura cartográfica.
[00:02:10] Não, não é um problema cartográfico, não é um problema geográfico.
[00:02:13] O problema surgiu no contexto de coloração de mapas.
[00:02:16] Mas de fato ele é um problema, ele é uma curiosidade matemática, estabelecer um número
[00:02:19] mínimo de cores e tudo mais, e especificamente quatro, também não sabe porquê, as razões
[00:02:23] de ordem psicológica.
[00:02:24] O fato é que esse problema foi informado a um membro da comunidade matemática, que
[00:02:30] era o De Morgan.
[00:02:31] E o De Morgan falou, olha, me deixa pensar, e começou a escrever umas cartas para uns
[00:02:35] colegas.
[00:02:36] E passou um tempo, inclusive tem uma resenha de um livro sobre divulgação científica
[00:02:41] em que ele faz uma nota de rodapé e comenta isso.
[00:02:44] E aí claro, isso recebeu uma formulação matemática, tanto em termos de topologia
[00:02:48] quanto em termos de teoria dos grafos, e mais tarde em termos de combinatória.
[00:02:51] Na verdade o problema tem várias formulações distintas, mas todas elas preservam essa
[00:02:56] característica de se perguntar pela possibilidade da existência de um mapa planar, normal e
[00:03:01] minimal.
[00:03:02] E aí começam todas as caracterizações.
[00:03:03] Pois é, isso que eu queria entender um pouco melhor.
[00:03:05] Em que condições vale o teorema, ou em que condições ele falha?
[00:03:09] Primeiro que só se trata de mapas no plano, e portanto não vale em mapas que não sejam
[00:03:14] planares.
[00:03:15] Existe alguma versão tridimensional?
[00:03:17] Por exemplo, células que também tem vizinhas?
[00:03:20] Não que eu saiba.
[00:03:21] Só para esclarecer um pouco sobre a questão dos mapas planares, o que que é vizinho?
[00:03:25] O que que é ser uma região adjacente?
[00:03:27] Adjacente é importante.
[00:03:28] Por exemplo, eu tenho um exemplo, eu estava falando com a Gisele antes de começar o programa,
[00:03:31] logo que eu vi que a gente ia fazer esse programa, e eu pensei, não, não é verdade.
[00:03:34] E aí o que eu fiz?
[00:03:35] Eu fui no Google e comecei a olhar imagens de, como é tiling, como é que é o tiling?
[00:03:41] Preenchimento, pavimentação.
[00:03:42] Preenchimento de superfície com figuras regulares.
[00:03:46] E aí tu começa a olhar e começa a pensar a respeito.
[00:03:48] Então, por exemplo, um exemplo claro para ver o que que é uma região contigo ou não
[00:03:51] é a gente pensar o tabuleiro do xadrez.
[00:03:54] O tabuleiro do xadrez a gente consegue pintar só com duas cores.
[00:03:57] Aí você vai dizer assim, ah tá, mas o preto de uma diagonal, ele encosta no preto a outra
[00:04:03] diagonal.
[00:04:04] Não vale se encostar, se encostar num ponto só, tu não considera adjacente.
[00:04:08] Então, tabuleiro de xadrez, só duas cores são suficientes.
[00:04:10] Tu tem que ter duas regiões adjacentes quando elas compartilham um lado.
[00:04:13] Um lado inteiro.
[00:04:14] E o outro lado tem que ter uma medida não nula, tem que ter um comprimento não zero.
[00:04:18] Não vale ser só um ponto.
[00:04:19] Então, se você tiver um círculo como uma fatia de pizza, é claro que nem todas as
[00:04:25] regiões são adjacentes umas das outras, porque não vale só um ponto.
[00:04:27] A fatia de pizza é interessante, a fatia de pizza só tem duas cores também.
[00:04:31] Exatamente.
[00:04:32] Tá, então assim, se o lado tiver comprimento zero, foi um ponto, não vale.
[00:04:37] Mas e se tiver comprimento infinito?
[00:04:39] Se a fronteira foi um fractal, por exemplo?
[00:04:41] Não sei, nunca pensei nisso.
[00:04:44] Essa é a segunda pergunta de físico, mas eu não tinha mais.
[00:04:47] É a generalização.
[00:04:50] Bom, então se trata de mapas planares e mapas normais, que é uma outra restrição, né?
[00:04:55] O que é um mapa normal?
[00:04:56] Um mapa normal é um mapa em que, por exemplo, não pode ter uma região isolada das outras,
[00:05:01] pensa no caso de Fernando de Noronha, o mapa do Brasil não é um mapa normal, ou mesmo
[00:05:05] nos Estados Unidos, porque além de ter o Havaí separado, além disso acho que tem
[00:05:09] o estado, se não me engano, de Michigan, que está dividido em duas regiões separadas,
[00:05:14] então também não pode ter uma região, por exemplo, você não pode ter uma região
[00:05:17] a aqui e uma região a aqui.
[00:05:18] Assim porque você teria que pintar ela com a mesma cor.
[00:05:21] Exato, então além de tudo você não pode ter regiões separadas, digamos, fisicamente,
[00:05:27] mas não é totalmente diferente.
[00:05:28] Então se tiver muitas delas, você vai ter que usar mais cores, é essa a ideia?
[00:05:31] É, porque todas elas, porque com essas condições, se tiver uma região separada ou se tiver
[00:05:37] ou dentro do mapa, uma região bifurcada em duas, você também já tem contraexemplos,
[00:05:43] então essas condições na verdade são para você eliminar os contraexemplos mais fáceis,
[00:05:48] a conjectura.
[00:05:49] Um mapa normal, por exemplo, você não vai ter uma região central, sabe quando a gente
[00:05:55] corta bolo na festa, que alguém corta um círculozinho no meio assim e depois faz
[00:06:00] a corte do bolo?
[00:06:01] Não pode ter uma região central circundada, por exemplo, por uma região inteira central
[00:06:04] também.
[00:06:05] Se for assim, não é um mapa normal, aí não pode, então essas são as três principais.
[00:06:09] Ou seja, você precisa ter vétis, você não pode ter uma fronteira sem nenhum vétil.
[00:06:14] Exato, pensa pra essa condição aqui.
[00:06:16] E quando é que deixou de ser uma conjectura, quando é que foi demonstrado?
[00:06:19] Bom, aí é que está todo um dos principais interesses filosóficos em torno do teorema.
[00:06:25] Então deixa eu voltar antes da gente entrar nessa parte que é mais…
[00:06:28] É porque eu ainda não dei a formulação, digamos, precisamente em termos de topologia,
[00:06:34] por exemplo.
[00:06:35] Então, o enunciado do teorema é todo o mapa planar normal, minimal, é admissivelmente
[00:06:41] quatro-colorível.
[00:06:42] O que é admissivelmente?
[00:06:44] Ser colorido com quatro cores, sem que nenhuma região já seja colorida com a mesma cor.
[00:06:48] E é um problema interessante, por exemplo, tu sabe que ele é colorível com quatro cores,
[00:06:55] agora se eu te dou um mapa em branco, do ponto de vista do teorema é irrelevante, mas pode
[00:07:00] ser um problema interessante pra alguma comunidade, o processo de colorir.
[00:07:06] Porque em matemática uma coisa é provar a existência da solução, a outra é encontrar
[00:07:11] a solução.
[00:07:12] Então, existe alguma informação sobre que tipo de problema é o processo de colorir,
[00:07:17] ele é solúvel em tempo polinomial, ele é um problema NP, completo?
[00:07:23] Eu acho que era N², não é?
[00:07:26] Então aí…
[00:07:27] Então, tem duas coisas separadas.
[00:07:29] Eu quero saber qual é a dificuldade de um algoritmo, ou algoritmo que porventura se
[00:07:37] ocupa de colorir, quanto tempo, em quantos passos ele consegue achar a solução em função
[00:07:44] do tamanho, do número de regiões.
[00:07:46] Porque claro, se eu te dou um mapa com cinco regiões, em alguns segundos tu pinta, mas
[00:07:51] se ele tiver quinhentas, o tempo vai crescer muito mais.
[00:07:54] Porque eu vi alguma coisa de que alguns mapas podem ser coloridos com três.
[00:08:00] Ah sim, tem o teorema, os outros tem o teorema de cinco cores, mas eu acho que de…
[00:08:06] E no caso de três, seria NP completo o problema?
[00:08:09] De toda maneira, o problema de de fato colorir mapas não é o problema que não tem a ver
[00:08:13] com o teorema, isso é um problema de aplicação, digamos assim.
[00:08:17] Então quanto a isso eu não tenho informações, eu nunca busquei isso, porque isso é um problema
[00:08:20] de aplicar, certo?
[00:08:22] Aqui na Wikipédia tem uma coisa que diz assim que algoritmos eficientes para quatro colorir
[00:08:30] mapas requerem somente N quadrado, onde N é um problema de tertes.
[00:08:36] Então é um problema fácil.
[00:08:37] Sim, desse ponto de vista ele é um problema fácil, mas é porque, aí de novo, essa
[00:08:40] pergunta, como eu disse que tinha dois elementos da tua pergunta, porque essa pergunta sobre,
[00:08:45] por exemplo, o tempo de computação que é necessário para e tudo mais, que está envolvido
[00:08:50] com a prova do Teorão das Quatro Cores, ela diz respeito somente a encontrar os casos
[00:08:54] que são necessários para a prova, porque no fim das contas, aí vem a parte interessante
[00:08:59] filosóficamente, o que importa é o modo como o resultado foi obtido, certo?
[00:09:03] O modo como esse teorema foi provado.
[00:09:06] E a razão pela qual esse teorema figura na comunidade matemática, na comunidade filosófica,
[00:09:11] desculpa, mas também na matemática, claro, em primeiro lugar na matemática, mas até
[00:09:14] hoje na filosófica, como um caso interessante de ser estudado, é o fato de que a prova
[00:09:20] depende essencialmente do uso de computadores, porque no tempo de uma vida humana não é
[00:09:26] possível realizar a prova do Teorema das Quatro Cores, ponto.
[00:09:30] Um ser humano não é capaz de realizar durante o tempo de uma vida humana a prova, por causa
[00:09:36] da quantidade de casos que são necessários para resolver uma prova por exaustão.
[00:09:40] Você está pensando no mesmo tipo de prova.
[00:09:41] Eu estou pensando na prova.
[00:09:42] Alguém pode descobrir uma demonstração que seja independente do computador.
[00:09:46] A demonstração que possivelmente seria encontrável, infinita, humanamente infinita,
[00:09:54] humanamente manuseável, ela precisa adotar outra estratégia.
[00:09:59] Então, se vocês me permitem uma consideração histórica, o que acontece é que em 1879 foi
[00:10:04] a primeira pretensa prova do Teorema das Quatro Cores apresentada, certo?
[00:10:09] E a estratégia dessa prova é a mesma estratégia das provas que são aceitas hoje, da prova
[00:10:16] de 1777, que é a prova do papel do Heikin.
[00:10:19] As outras formulações mais recentes que existem, existem em duas versões, em 1976, todas essas
[00:10:27] provas, por mais rápidas, por mais que elas sejam feitas com outros algoritmos até a
[00:10:31] última prova, ela está completamente formalizada e ela foi feita com aquele provador de Teorema
[00:10:36] chamado Coq, o Provador Automático de Teoremas, Coq, que é galo francês.
[00:10:45] Então, foi feita toda com esse Provador Automático de Teoremas, é uma prova muito menor, ao
[00:10:49] invés de quase 1800 casos, são 400 e poucos casos, mas de todo modo, a estratégia, meu
[00:10:56] ponto é, a estratégia geral ainda é a mesma estratégia utilizada por esse senhor chamado
[00:11:02] Camp, da British Mathematical Society, que foi quem anunciou essa pretensa prova.
[00:11:07] Aprovei o Teorema.
[00:11:08] Como era a prova?
[00:11:09] Em primeira, a primeira característica é uma prova por redução absurda, portanto,
[00:11:14] essa com a hipótese de que existe pelo menos um mapa, cinco cromático, minimal, admissivelmente
[00:11:21] quatro colorível, certo, e então você, a partir da suposição de que existe um,
[00:11:27] que somente cinco cores são necessárias para colorir todo o mapa, você, através de
[00:11:31] uma própria indução, que o mínimo número de cores é cinco, para colorir qualquer mapa,
[00:11:36] tá, sim, você vai, você, a partir disso, você vai por exaustão, fazendo uma série
[00:11:42] de casos e encontrando, tal, de método de redução que ele desenvolveu, uma maneira
[00:11:47] de encontrar a contradição, que é o quê?
[00:11:48] Que é mostrar que esse mapa que é colorido só com quatro, cinco cores e que supostamente
[00:11:53] é o menor possível, por isso ele é minimal, ele pode ser reduzido.
[00:11:57] Ah, ele pode ser pintado com quatro cores.
[00:11:59] Exato.
[00:12:00] E aí é que vem a contradição e aí você nega a hipótese, bom, então prova.
[00:12:03] Então ele gera, ele gera todo, é como se ele gerasse todos os mapas de cinco cores
[00:12:08] reduzidos.
[00:12:09] Que ser redutíveis.
[00:12:10] Ele diz que tem um mapa que só pode ser pintado com cinco, e daí ele conclui que esse mesmo
[00:12:14] mapa pode ser pintado com quatro.
[00:12:15] Com quatro, isso.
[00:12:16] Sim, sim, mas ele não pode fazer só para um, ele tem que fazer para um grupo de mapas
[00:12:20] que representam todos os possíveis mapas de cinco cores.
[00:12:22] E ele fez isso através de uma estratégia que, ele fez o quê?
[00:12:26] Ele começou então supondo que cinco são necessárias e que esse mapa, cinco cromático,
[00:12:31] pentachromático, normal, é o menor, então ele é minimal.
[00:12:34] Aí ele falou assim, olha, todo mapa, todo mapa, cinco cromático, normal, minimal, tem
[00:12:41] que ter pelo menos quatro tipos de configurações.
[00:12:43] E aí ele provou certos lemas.
[00:12:45] Para o caso de duas cores é mais fácil, mas para o caso de três, quatro e cinco cores,
[00:12:49] ele provou que dava para reduzir.
[00:12:51] E ele reduzi, como é que ele provou essa redutibilidade?
[00:12:55] Mostrando que figurava em cada uma desses tipos de configuração, uma dentre quatro
[00:13:01] configurações possíveis, certo?
[00:13:04] Então, a estratégia consiste basicamente na prova em construir um conjunto inevitável
[00:13:09] de configurações que são redutíveis.
[00:13:11] Que são irredutíveis?
[00:13:13] Irredutíveis, claro, porque todo mapa tem que conter pelo menos uma delas.
[00:13:16] Assim, ou seja, qualquer mapa que eu pego, por exemplo, se eu pego o mapa da A.
[00:13:20] Ele tem que conter pelo menos uma dessas quatro configurações.
[00:13:22] Ou seja, e se eu reduzo ele para algum processo formal, ele vai cair numa dessas categorias.
[00:13:29] A única coisa que você precisa é provar o problema para as categorias, se não precisa
[00:13:34] para os mapas individuais.
[00:13:36] A estratégia é essa, até hoje.
[00:13:38] Só que as categorias, inicialmente, eram 1400.
[00:13:41] Não, nessa prova que não era uma prova, porque estava errada, eram só quatro.
[00:13:44] O conjunto de configurações redutíveis era apenas composto por quatro.
[00:13:49] Estava errada por causa da prova do último lema, que era do caso de uma região com cinco
[00:13:56] vizinhas, fazer um método de redução dela tinha um problema que ele não percebeu.
[00:14:02] Dez anos depois, o erro foi percebido.
[00:14:04] Isso foi quando?
[00:14:05] 1889.
[00:14:06] E aí, dez anos depois, só que esse erro foi percebido, e aí as pessoas começaram
[00:14:12] a se engajar novamente na comunidade matemática a tentar resolver o problema.
[00:14:15] E aí, pulou ao invés de quatro configurações irredutíveis, foi para 1400, e por isso precisa
[00:14:19] do computador.
[00:14:20] Para construir essas, porque o que o computador ajuda a fazer?
[00:14:24] O computador ajuda a construir o conjunto inevitável, porque todo mapa tem que ter,
[00:14:29] de configurações redutíveis, certo?
[00:14:31] E aí depois o computador também ajuda a colorir elas e mostrar que dá para…
[00:14:35] Não.
[00:14:36] Não?
[00:14:37] Porque é isso, é justamente essa parte de colorir e de mostrar.
[00:14:40] Porque veja, ele só se tornou um problema computacionalmente tratável quando você,
[00:14:44] historicamente falando, passa da abordagem, você faz duas passagens dentro da matemática.
[00:14:51] A teoria de topologia é a teoria dos grafos, porque se você imaginar aqui, vocês sabem
[00:14:55] disso, que vocês podem imaginar que as regiões têm as capitais, e aí tem, digamos, metaforicamente
[00:15:00] falando as estradas que conectam as capitais, que seriam…
[00:15:04] Ou seja, transforma o problema das regiões num problema de um grafo.
[00:15:07] Do grafo e depois…
[00:15:08] O grafo seria basicamente um conjunto de pontos ligados por linhas.
[00:15:12] Isso.
[00:15:13] Mas não pode ser todo grafo.
[00:15:14] Não pode ser qualquer grafo.
[00:15:15] Justo, tem que ser todo grafo, um grafo que mantém as mesmas características daquelas
[00:15:20] características que o mapa tinha que ter, um mapa planar, normal, minimal, e isso vai
[00:15:23] ser traduzido na linguagem dos grafos.
[00:15:25] É, porque se eu pegar, por exemplo, um grafo que represente a internet, ele tem propriedade
[00:15:29] de interações de longa ou careta que não pode.
[00:15:32] Que não pode.
[00:15:33] Não, os grafos vão ter tantas limitações quanto tinha os mapas lá, aquelas condições
[00:15:36] que a gente colocou.
[00:15:37] São grafos correspondentes a esses mapas, e aí, onde é que os computadores entram em
[00:15:43] cena?
[00:15:44] Quando você faz a passagem de grafos para combinatório, porque aí se trata simplesmente
[00:15:48] do que?
[00:15:49] De calcular as combinações possíveis.
[00:15:50] Então, deixa de ter o problema de colorir, esquece, acabou cor, não tem mais, agora
[00:15:54] é só uma questão de combinatório.
[00:15:56] E aí que os computadores entram em cena, entende?
[00:15:58] Ajudar a fazer as contas, é como uma espécie de bloco de notas aperfeiçoado, no caso
[00:16:05] do uso do computador nessa prova.
[00:16:07] E quanto tempo leva o computador para fazer a demonstração?
[00:16:09] Depende do computador.
[00:16:10] Da prova original, ela foi descoberta em 1976 e publicada em 1977, foram mais de 1.200
[00:16:22] horas de computação, com os computadores de 1977, na Universidade de Linoim.
[00:16:28] Hoje se faz no celular.
[00:16:30] Claro.
[00:16:31] E esse tempo todo foi o tempo para construir o tal conjunto que tem 1.498 configurações.
[00:16:40] Que todo mapa dessa categoria tem que ter.
[00:16:43] E então, como eu dizia, a razão pela qual essa prova se torna interessante para filósofos
[00:16:49] que gostam de estudar matemática, filósofos da matemática, é o fato de que pela primeira
[00:16:54] vez tu tens a prova de um teorema matemático que não é humanamente produzível do início
[00:17:00] ao fim e nem verificável.
[00:17:02] Porque aí entra um outro aspecto importante para quem estuda filosofia da matemática
[00:17:06] e das ciências, porque tradicionalmente a matemática é vista como campo de saber
[00:17:11] em que só valem procedimentos, que os filósofos gostam de chamar de procedimentos a priori,
[00:17:15] que significa sem o apoio da experiência empírica.
[00:17:19] Prova é uma coisa, experimento é outra coisa.
[00:17:21] E a prova do Teorema das Quatro Cores foi vista num primeiro momento pela comunidade
[00:17:25] filosófica como sendo uma prova experimental, o que para certos filósofos é um simples
[00:17:30] absurdo porque prova e experimento é uma distinção categorial, não pode ter uma
[00:17:34] prova experimental, e para outros não, significou um novo momento na história da matemática.
[00:17:39] Não é completamente e puramente um processo de dedução, ela tem esse caráter híbrido.
[00:17:45] Exatamente híbrido é a palavra que foi utilizada no artigo que deu origem a todo debate filosófico
[00:17:50] para um artigo de 1979 sobre o significado filosófico da prova e o autor, um tal Thomas
[00:17:55] Timóseco, ficou famoso unicamente por esse artigo.
[00:17:59] Ele fala exatamente que se trata de um híbrido entre prova e experimento.
[00:18:03] Por que?
[00:18:04] Primeiro lugar, porque se trata da introdução de uma máquina, e seja, ele também não tinha
[00:18:08] muita notícia sobre o que eram os computadores, como funcionavam, então para ele o fato de
[00:18:11] que você tem uma máquina fazendo o trabalho de um ser humano já serve de ponto para esse
[00:18:17] argumento dele, que eu chamei de argumento da introdução da experimentação na matemática.
[00:18:21] Um dos pontos é, olha, você tá, não é só um ser humano que pode fazer dedutivamente
[00:18:24] a priori.
[00:18:25] Segundo lugar, parece um experimento também porque eles construíram o algoritmo para
[00:18:31] construiu o conjunto inevitável de configurações redutíveis, por tentativa errou, óbvio,
[00:18:35] eles tentavam, eles construíram um conjunto, testavam para ver se os membros do conjunto
[00:18:39] eram redutíveis, não era, eles voltavam, refaziam o algoritmo, construíram um outro
[00:18:44] conjunto, testavam para ver se era redutível, não era, eles refaziam o algoritmo.
[00:18:48] Bom, para esse senhor Timóseco, isso era um ponto a favor da ideia de que, bom, tá
[00:18:52] vendo, os matemáticos estão procedendo igual nas ciências experimentais, estão tentando
[00:18:56] voltando.
[00:18:57] O algoritmo também foi um resultado da pesquisa, ele não era nem, ele não foi, não é assim,
[00:19:02] eu sei qual é o algoritmo que me dá a resposta certa e o computador vai calcular.
[00:19:06] Não, ele foi construído com o auxílio do computador, o próprio algoritmo.
[00:19:09] Então esse é um ponto, como é que o computador foi usado naquilo que a gente gosta de chamar
[00:19:13] de contexto de descoberta, ele foi usado no contexto de descoberta para descobrir o algoritmo.
[00:19:19] Mas aí que aconteceu, veja, em 1967, certo, não tinha prova formal de que o algoritmo
[00:19:25] era formalmente correto, completo, não tinha contradição.
[00:19:29] Então o que eles fizeram?
[00:19:30] Uma vez que eles não têm a prova formal de que o algoritmo é definitivamente completo,
[00:19:34] consistente, tudo isso, eles tiveram que rodar em outros computadores o mesmo algoritmo agora.
[00:19:40] Então para um filósofo olhando de fora sem entender muito bem como funciona a ciência
[00:19:43] da computação, ele não falando do que ele tá vendo, eles estão fazendo exatamente
[00:19:46] como um cientista que faz o experimento uma vez, fica feliz com o resultado, mas não
[00:19:51] está satisfeito, porque ele precisa fazer mais uma vez e mais uma vez para confirmar
[00:19:54] o resultado.
[00:19:55] Porque ele só está testando se os computadores não têm problemas, porque trocar o computador,
[00:20:01] e se o problema fosse no algoritmo, se tivesse um problema no algoritmo, tu teria que fazer
[00:20:05] a mesma coisa com algoritmos escritos por mim, por ti.
[00:20:09] Exato, e é por isso que eu escrevi a tese de doutorado que eu escrevi, porque me parece
[00:20:14] que a partir desse artigo em que essas coisas estão muito confusas, mas esse artigo deu
[00:20:20] o início a uma discussão filosófica que, num certo sentido, vai até hoje, a minha
[00:20:24] tese foi uma tese que foi escrita para tentar o que?
[00:20:26] Fazer um mapa dessas discussões e ver que tipo de esclarecimento precisa ser feito para
[00:20:30] dissipar certas confusões, como por exemplo, você não está fazendo o teste no mesmo
[00:20:34] sentido que você faz um teste no âmbito empírico.
[00:20:37] Então a dúvida era se esse procedimento que estava sendo feito de alguma forma como
[00:20:42] uma espécie de caixa preta, o quanto ele era confiado?
[00:20:46] Porque saiu da mão do matemático, o ser humano, fazer o teste, quando você mete
[00:20:51] o teste no artigo em matemática, tem alguém que vai lá e vai repetir a conta, vai testar,
[00:20:55] e agora é uma máquina, e a máquina você não sabe o que está fazendo.
[00:20:57] A máquina ajudou a produzir o algoritmo e a máquina depois foi usada para testar para
[00:21:02] ver se dava o mesmo resultado.
[00:21:05] Se dava o mesmo resultado.
[00:21:06] Isso parece uma pergunta meio absurda, porque o seu algoritmo é o mesmo, porque algoritmo
[00:21:11] para mim é uma série de instruções escritas numa língua, e onde você roda vai sair a
[00:21:18] mesma coisa.
[00:21:19] Você precisa testar se o algoritmo foi escrito corretamente, então eu não vou te mostrar
[00:21:23] o meu e você vai fazer o mesmo, supostamente o mesmo, mas do teu jeito, tem que dar a mesma
[00:21:28] coisa.
[00:21:29] Mas a questão é que o algoritmo, a partir do algoritmo, não dá para fazer nenhum teste
[00:21:35] matemático, não, esse algoritmo é o que eu preciso.
[00:21:38] Não pode?
[00:21:39] Ou seja, você pode usar o algoritmo no contexto da justificação, essa é a pergunta, pode
[00:21:43] usar o algoritmo para justificar ele mesmo?
[00:21:45] A maioria que entra toda a celeuma em torno dessa prova, porque em princípio quando a
[00:21:50] prova foi apresentada pela primeira vez no encontro no Canadá, a plateia se dividiu
[00:21:56] em duas, os mais novos ficaram fascinados, muito curiosos perguntando como é que era
[00:22:02] possível acreditar numa prova que continha tantas páginas e tantas microfichas e tantos
[00:22:10] anexos, que era tão longo assim, mas aceitavam que era um resultado, enquanto os mais velhos
[00:22:16] diziam, como é possível acreditar numa prova que foi produzida por um computador?
[00:22:20] Então num certo sentido, e esses que fizeram, os últimos, como é possível acreditar numa
[00:22:25] prova que foi quase toda feita com o auxílio de um computador, para eles estava em jogo
[00:22:31] justamente o conhecimento de como é que o computador funciona, qual é o papel do computador
[00:22:36] nesse processo.
[00:22:37] É muito relevante aí o entendimento do que é um algoritmo, o que é a função do computador.
[00:22:42] E os mais antigos, se você pensar na divisão da plateia, os mais antigos talvez por falta
[00:22:47] de interesse ou de familiaridade tiveram um tipo de reação muito negativa.
[00:22:51] Porque eu vejo bem diferente do caso, por exemplo, do agora aprovado o último teorema
[00:22:54] de Fermat.
[00:22:55] Isso.
[00:22:56] Então esse é um problema que demorou, sei lá, 200 anos para ser resolvido, mas antes
[00:23:00] dele ser resolvido formalmente, como os matemáticos gostam, existia um experimento de computador.
[00:23:06] E aí eu vejo o que é um experimento de computador, porque um experimento de computador, um experimento
[00:23:10] na minha opinião, é uma coisa que não esgota as possibilidades.
[00:23:14] O que era naquela época o experimento de computador?
[00:23:16] Eles ficavam testando os números, que era um pouco para aumentar a verossimilhança,
[00:23:21] a nossa expectativa sobre…
[00:23:22] É, porque quando você tem uma conjectura, basta um contra exemplo para eliminar tudo.
[00:23:28] Eles testavam para conjuntos de três inteiros cada vez maiores, cada vez maiores, cada vez
[00:23:32] maiores e nunca achavam um contra exemplo.
[00:23:35] Então isso aumentava a confiança no teorema, mas não provava o teorema.
[00:23:38] Isso.
[00:23:39] E isso no caso do teorema das clássicas foi completamente diferente, porque em princípio
[00:23:43] o algoritmo esse está esgotando as configurações irredutíveis.
[00:23:47] Porque a fissão é um conjunto finito.
[00:23:49] É um conjunto finito.
[00:23:50] Então esse é o experimento, eu não chamo de experimento de computador, isso é um teorema
[00:23:53] aprovado para o computador.
[00:23:55] É um processo de enumeração.
[00:23:56] Isso, exatamente.
[00:23:57] Exatamente.
[00:23:58] Mas aqui tem que levar em conta que no momento que isso aconteceu, era exatamente quando
[00:24:04] os computadores estavam começando a ser introduzidos em larga escala.
[00:24:08] Naquele momento os computadores eram institucionais, não existia.
[00:24:11] Exato.
[00:24:12] No Instituto de Física, por exemplo, quando a gente se mudou aqui para o campus do Vale,
[00:24:16] eles botaram uma tomada por sala e disseram quem é que vai precisar mais do que uma tomada
[00:24:20] por sala.
[00:24:21] E agora a gente tem problemas.
[00:24:22] É curiosa essa tua observação, porque quando tem um trabalho de um sociólogo americano,
[00:24:28] o livro inteiro é sobre computadores, provas e tudo mais, e tem um capítulo dedicado à
[00:24:33] história do Teorema dos Quatro Cores, e ele conta coisas anedóticas, por exemplo,
[00:24:37] o pessoal que desenvolveu, a equipe do Apple, do Haken, que desenvolveram a prova, já
[00:24:40] estavam há mais de dez anos envolvidos com o problema e tal.
[00:24:44] Eles tiveram que fazer muitas relações, estabelecer certas relações políticas dentro da universidade
[00:24:49] para conseguir o computador emprestado durante a noite, porque o computador era usado para
[00:24:53] coisas importantes durante o dia, e aí eles passavam a noite inteira fazendo com computadores
[00:24:59] gigantescos, assim, e até isso demandou certas… parece que um deles era muito bem relacionado
[00:25:04] com a reitoria e tal, e aí conseguiu emprestar os computadores durante a noite para poder
[00:25:08] rodar e fazer os testes e construir o algoritmo.
[00:25:10] Imagina se nem dentro da matemática aquilo era considerado um procedimento sério, imagina
[00:25:16] tirar o tempo de engenharia, para desenvolver coisas importantes.
[00:25:21] E de lá para cá mudou um pouco essa atitude em relação a esse tipo de demonstração?
[00:25:25] Eu entendi de quem, assim, na tese, no final do primeiro capítulo, que é quando eu apresento
[00:25:29] um pouco de estratos de história e as ideias principais da prova, então eu escrevi um
[00:25:34] capítulo assim do tipo, o Teorema das Quatro Cores for Dummies, só que na verdade é para
[00:25:39] filósofos, né?
[00:25:40] Então no final do primeiro capítulo o que eu faço é apresentar as primeiras reações
[00:25:44] e respostas e dividir o grupo das reações entre a comunidade de matemáticos e a comunidade
[00:25:51] dos informáticos, porque eles também tinham críticas, por exemplo, o alfático algoritmo
[00:25:55] que não foi verificado formalmente, e a comunidade dos filósofos.
[00:25:58] A principal é que o pessoal da computação naquela época era quase todos um da matemática
[00:26:02] também, né?
[00:26:03] Um deles, uma das pessoas da equipe era a engenheira, um dos principais era a engenheira, mas de
[00:26:08] todo modo sim, é uma área, né?
[00:26:10] É uma área mais próxima, com certeza mais do que a filosofia.
[00:26:14] Então tem a reação da comunidade matemática e da comunidade dos informáticos e tem a
[00:26:18] reação dos filósofos.
[00:26:19] A meu ver, a comunidade dos matemáticos e dos informáticos hoje em dia já não considera
[00:26:24] como um problema esse caso específico, e mesmo casos mais em que você tem resultados
[00:26:31] que o computador participa de maneira muito mais significativa do que como um bloco de
[00:26:36] notas, como foi o caso aqui.
[00:26:38] Então me parece que, claro, alguma polêmica ainda há, né?
[00:26:41] Alguns achando que a matemática é uma coisa que, de fato, depende essencialmente de intuições
[00:26:45] e de certa inteligência que os computadores jamais vão ter, mas mesmo assim, a área
[00:26:50] de demonstrações assistidas por computadora hoje ela é uma área, eu acho, mais ou menos
[00:26:55] relativamente tranquila dentro da matemática.
[00:26:59] Não me parece que haja tanto problema, assim, a não ser político e ideológico, certo?
[00:27:04] Então assim, existem do universo das provas matemáticas, existe uma parcela com as provas
[00:27:08] auxiliadas computacionalmente, inclusive existe esse jornal, esse Journal of Experimental
[00:27:15] Mathematics.
[00:27:16] Tem até uma área, que é a área da matemática experimental, que basicamente é a matemática
[00:27:21] feita com computadores, e existe uma polêmica sobre isso, mas o caso, Teremos Quatro Cores,
[00:27:25] acho que ele é uma curiosidade histórica, e tal, para a comunidade matemática e para
[00:27:28] a comunidade informática.
[00:27:29] Para a comunidade filosófica, volta e meia ele é trazido à tona de novo, por quê?
[00:27:34] Porque alguns ainda estão preocupados com problemas de demarcação de conhecimento,
[00:27:39] então é importante discutir casos como esse, porque seria um caso em que você poderia
[00:27:43] dizer que agora tem experimento dentro da matemática ou não e tudo mais.
[00:27:46] A definição de prova matemática, como a prova é a coisa mais importante para o uso.
[00:27:49] Mas mesmo dentro da matemática, hoje em dia é um novo trend, que se chama Filosofia
[00:27:54] da Prática Matemática.
[00:27:55] E para os filósofos da prática matemática, que diferentemente dos filósofos chamados
[00:28:00] fundacionalistas, que estavam preocupados com os fundamentos da matemática, uma tradição
[00:28:04] que remonta a Frege, Hilbert e Brouwer, tudo mais, no início do século XX, para os filósofos
[00:28:09] fundacionalistas da matemática era importante, portanto, dizer quais são os fundamentos,
[00:28:13] se são lógicos, se são intuitivos.
[00:28:14] Para os filósofos da prática matemática, o que importa é de fato o que os matemáticos
[00:28:18] fazem.
[00:28:19] E para eles, se os matemáticos incorporam o computador na vida da matemática, então
[00:28:23] o que cabe a gente fazer?
[00:28:25] Descrever esses usos.
[00:28:26] Para o que eles são usados, é para calcular ou é só para calcular ou é para de fato
[00:28:30] construir provas e coisas do tipo?
[00:28:32] Então, para a gente interessa, por exemplo, distinguir cálculo de experimento e de prova
[00:28:37] para poder ter um pouco mais de clareza, eu diria que caso tenhamos quatro cores é interessante,
[00:28:41] porque ele abre a possibilidade de interessantes investigações sobre filosofia da computação.
[00:28:47] Quer dizer, a filosofia metendo o B dele em mais uma área da vida humana, mas eu tento
[00:28:53] não ser chata.
[00:28:54] Mas é que existem vários tipos de chatice, quem conhece o tratado geral dos chatos, não
[00:29:00] é um livro maravilhoso.
[00:29:01] Mas enfim, existem vários tipos de chatice, então a chatice do filósofo é meter o B
[00:29:03] dele em tudo do ponto de vista conceitual.
[00:29:06] Evidentemente, nós tratamos jamais de dizer que o que o matemático faz está certo ou
[00:29:09] errado, porque a gente simplesmente não tem habilidade e conhecimento para isso.
[00:29:12] Acho que é preciso que fique claro, a gente só quer analisar a dimensão conceitual das
[00:29:17] atividades dos outros e jamais colocar o nosso B dele no sentido de dizer que está certo
[00:29:22] ou errado.
[00:29:23] Embora, no caso da discussão sobre a prova de teramos quatro cores, muitas vezes aconteceu
[00:29:27] dos filósofos dizerem, olha, estão enganados, isso é um experimento, não é uma prova.
[00:29:31] E eu tentei mostrar na tese que isso é absolutamente equivocado, que a gente tem que se manter
[00:29:34] no nosso lugar do esclarecimento conceitual.
[00:29:37] Tá bom, então.
[00:29:38] Então hoje a gente teve aqui a Gisele Seco, que é a professora aqui do Departamento
[00:29:41] de Filosofia da URGS, e mostrando que uma coisa tão simples como pintar mapas gera
[00:29:46] tanta discussão, só entre os filósofos, claro, entre nós físicos, a gente já sabia
[00:29:50] o resultado.
[00:29:51] É óbvio o resultado.
[00:29:52] Exato.
[00:29:53] Então os participantes do programa foram o pessoal daqui, né, eu, o Marco de Arte
[00:29:57] e o Jefferson Elzon, do Departamento de Física da URGS.
[00:30:00] O Programa Fronteiras da Ciência é um projeto do Instituto de Física da URGS, direção
[00:30:06] técnica de Francisco Gwazel.
[00:30:08] Porque tu obtém o resultado, também não te diz nada.
[00:30:17] Claro.
[00:30:18] O mesmo podia acontecer com um resultado tradicional.
[00:30:20] Tu tem que conversar com o resultado, tem que conversar com o resultado da simulação
[00:30:24] e ver o que é que ele decidiu.
[00:30:25] Imagina que o Andrew Wiles estivesse aqui e apresentasse pra gente a prova do último
[00:30:29] terreno de Fermat.
[00:30:30] É, basta olhar a demonstração.
[00:30:32] E aí tem um aspecto que pra mim é interessante, e eu exploro em algum momento também do trabalho,
[00:30:37] que é, tem um aspecto da prática dos matemáticos e da prática dos físicos e todo mundo que
[00:30:41] lida com demonstrações, que é um aspecto, digamos assim, retórico, no sentido da boa
[00:30:46] e velha retórica clássica, em que você precisa levar em conta o público com quem você
[00:30:50] tá falando.
[00:30:51] Então se eu vou apresentar, veja, eu apresentar a prova do terreno das quatro cores é algo
[00:30:54] que eu só posso fazer porque eu entendi os conceitos principais, os procedimentos principais,
[00:30:58] mas eu não sei nenhum detalhe.
[00:30:59] Se o matemático apresentar pra mim todos os detalhes, eu não vou entender tudo.
[00:31:03] Se o matemático explicar pra outro matemático da mesma área, ele vai entender.
[00:31:07] Se o matemático explicar pros seus alunos, ele vai ter que mudar.
[00:31:10] Então tem esse aspecto que eu chamo de aspecto retórico, um aspecto social, que tem a ver
[00:31:15] com pra quem você tá apresentando o resultado e o que você tá fazendo.
[00:31:18] Se ele tá no âmbito da divulgação, ele vai falar.
[00:31:20] Mas isso é uma tradução que é feita, ou seja, tu tem a prova e dependendo do contexto
[00:31:25] tu precisa fazer uma tradução, mas essa tradução pode gerar uma não-prova.
[00:31:29] Então, se eu tô explicando aquela prova pro físico, como nós, talvez aquilo ali
[00:31:34] não seja suficientemente rigoroso pra ser considerado uma prova, aquela explicação.
[00:31:38] Então não é toda maneira de explicar, de contar que tem a mesma informação.
[00:31:43] Sim, mas eu acho que no caso da matemática, o caso que a Gisele falou do último Teorema
[00:31:47] de Fermat, não tem possibilidade de simplificação dessa prova que seja uma prova.
[00:31:51] A única prova mesmo é a prova mesmo que tem cento e tantas páginas.
[00:31:55] Não, pode ser que alguém apareça com uma demonstração mais simples.
[00:31:58] Mas, no momento, a simplificação…
[00:32:01] Ah, isso que eu falei, esse comentário, tu disse que existe a retórica e tem uma forma de…
[00:32:06] Aspecto retórico.
[00:32:07] É, um aspecto retórico, mas tem uma forma de tu te comunicar com o aluno, tem a forma
[00:32:11] de te comunicar com o leigo, e agora a gente introduziu uma nova, uma nova entidade que
[00:32:16] é o computador.
[00:32:17] O computador se comunica com o matemático de um jeito também, ele sabe a prova.
[00:32:21] O matemático não tem jeito de seguir a prova do computador.
[00:32:24] Então, lá vem o filósofo com as suas distinções.
[00:32:27] Verificar pode ter vários sentidos, né?
[00:32:29] Uma das coisas que eu também fiz no trabalho quando eu tava me deparando com essas discussões
[00:32:34] é que, por exemplo, no artigo original, que deu origem a toda a seleuma filosófica,
[00:32:38] ele vai dizer, o problema é que a prova não é inspecionável.
[00:32:41] Não é inspecionável passo a passo por um ser humano no tempo de uma vida humana.
[00:32:46] Entretanto, os computadores realizaram o cálculo.
[00:32:49] O que não é inspecionável é o trabalho do computador.
[00:32:51] Mas, inspecionável em que sentido?
[00:32:53] Não é inspecionável no sentido de que eu não posso acompanhar todos os passos calculatórios
[00:32:58] que o computador fez, mas eu sei o algoritmo.
[00:33:00] Então, num certo sentido, é inspecionável, sim, o que eu tentei fazer é distinguir os
[00:33:05] dois sentidos.
[00:33:06] Um sentido é verificabilidade algorítmica, e isso não dá para um ser humano fazer sozinho
[00:33:11] no tempo de uma vida humana.
[00:33:12] Outro sentido é o que a gente chama de sinopticidade, né?
[00:33:16] A ideia de você ter uma visão sinoptica por quem está de posse do algoritmo, compreende
[00:33:21] ele e seria capaz, se tivesse tempo de reproduzi-lo, essa pessoa, a gente pode dizer, ela pode
[00:33:27] inspecionar nesse sentido de ter uma visão sinoptica do procedimento, uma sinopse, uma
[00:33:32] imagem que contém tudo que você precisa para entender a coisa.
[00:33:35] Mas por que essa exigência de que seja uma pessoa?
[00:33:38] Por que eu não posso paralelizar?
[00:33:40] Porque mesmo o tema de Fermat, que tem, sei lá, 500 páginas de demonstração, não
[00:33:43] precisa dizer que um único matemático faça o controle, eu posso dizer, olha, eu tenho
[00:33:48] essas 5 coisas que são independentes, mas que depois se juntam para demonstrar, e eu
[00:33:52] tenho o fulano que pega para tear ou atrabiar e assim por diante.
[00:33:55] Aqui, que ainda é uma listagem de vários casos, eu posso distribuir por várias pessoas.
[00:33:59] Então é só uma questão de reescalar o tempo, porque se eu pegar várias pessoas fazendo
[00:34:03] em paralelo, elas conseguem reproduzir, então, em princípio, eu posso controlar tudo que
[00:34:08] foi feito.
[00:34:09] A resposta para a tua pergunta depende de uma consideração acerca do que tradicionalmente
[00:34:13] se faz em filosofia da matemática.
[00:34:15] Uma das coisas é investigar o conceito de demonstração, e de acordo com uma certa
[00:34:20] concepção tradicional de demonstração, uma demonstração é o que?
[00:34:23] É uma sequência de passos tais que os passos ou são axiomas ou são definições que você
[00:34:29] vai manipulando por regras de inferência e que um ser humano pode proceder do começo
[00:34:33] ao fim.
[00:34:34] Eu não estou defendendo que tenha que ser assim, é que tradicionalmente se pensou
[00:34:37] que uma prova matemática era isso, é algo que um ser humano consegue acompanhar do
[00:34:40] começo ao fim, partindo de definições, axiomas e princípios usando regras de inferência.
[00:34:45] Então, a tua pergunta é muito boa porque ela faz a gente perceber o conceito de prova
[00:34:49] que tradicionalmente era aceito, e o que tu está dizendo é bom, talvez pudesse haver
[00:34:53] uma modificação no sentido de que agora a gente poderia pegar uma coisa que é só
[00:34:57] quantitativamente muito complicada, combinatoriamente muito complicada e fazer essa divisão de
[00:35:01] trabalho.
[00:35:02] Eu tinha um professor que brincava, ué, pega um monte de chineses e peça para que eles
[00:35:05] dividam o trabalho.
[00:35:06] Porque ela é contraditória com a própria definição formal de matemática, porque
[00:35:10] quando eu vou demonstrar um teorema, eu posso me valer de um outro teorema que já foi demonstrado
[00:35:14] por outra pessoa.
[00:35:15] Então, é válida essa fragmentação em pedaços, esse resultado foi testado pelo fulano.
[00:35:21] Não preciso testar todos os teoremas.
[00:35:23] Mas no final tu tem que ter uma imagem completa do procedimento, não.
[00:35:26] Você não pode comunicar o procedimento de combinator.
[00:35:28] Depende de como você define completo.
[00:35:29] Se completo significa entender inclusive os teoremas que foram usados, nunca ninguém
[00:35:34] vai ter.
[00:35:35] O que eu estou dizendo é que o processo de demonstração de matemática, como usa outros
[00:35:38] teoremas, não tem uma pessoa controlando desde os axiomas até o final.
[00:35:43] Não tem uma um pouco de alta contradição?
[00:35:46] Não sei se diria contradição, porque essa palavra é muito repelante, mas a gente teria
[00:35:50] que conversar um pouco mais sobre em que medida resultados prévios que são incorporados
[00:35:54] em resultados atuais podem ser, em que medida eles são parte constitutiva da prova e tudo
[00:36:00] mais.
[00:36:01] Mas me parece que a gente não tem faz muito tempo.
[00:36:02] É só uma pergunta rápida.
[00:36:03] Então, foi o primeiro teorema a ser demonstrado usando essas técnicas híbridas ou existem
[00:36:08] muitos?
[00:36:09] Esse foi o único?
[00:36:10] Desde a década de 50, já tinha alguns teoremas, mas que não eram provavelmente matemáticos.
[00:36:15] Alguns teoremas, acho que os 38 primeiros teoremas do Prinkipia Matemática, do Russell
[00:36:18] e do Whitehead, já estavam sendo feitas provas mecanizadas desses teoremas.
[00:36:22] Só que eles eram teoremas que já estavam provados lá no Prinkipia e era muito mais
[00:36:27] para o fim, para ver o que acontecia, para ver o tempo e tudo mais.
[00:36:30] Então, já tinha provas sendo feitas de teoremas lógico-matemáticos antes.
[00:36:34] O problema é que no caso do Teorema dos Quatro Colores, não havia solução antes
[00:36:38] e a primeira solução foi gerada pelo computador.
[00:36:41] Então, por isso que ela foi curiosa.
[00:36:43] Mas teve outros casos depois?
[00:36:45] Depois, tem outros casos.
[00:36:46] Teve, inclusive, um volume da Notices of the American Mathematical Society de dezembro
[00:36:50] de 2008, que é especial sobre provas assistidas por computador, provas formais, e ela tem
[00:36:55] uma lista imensa de resultados.
[00:36:57] Todos os resultados, assim, chamados da matemática experimental, dependem disso.
[00:37:00] A curiosidade do ponto de vista filosófico é um pouco histórica, um pouco filosófica
[00:37:05] E a meu ver tem muito a ver com a necessidade que o filósofo tem de prestar atenção no
[00:37:09] que o matemático faz e, no caso específico, do Teorema dos Quatro Colores, é de também
[00:37:13] incluir não só o que o matemático faz, mas agora o que essa máquina faz.
[00:37:17] Que tipo de máquina é o computador, o que que é um programa, o que que é a implementação,
[00:37:22] qual é a relação entre hardware, software e perguntas dessa nova área que se chama Filosofia
[00:37:27] da Computação, e que é super interessante porque os próprios informáticos e o pessoal
[00:37:32] da comunidade da ciência da computação não parecem ter, assim, clareza sobre o uso
[00:37:37] desses conceitos que são fundamentais pra eles.