O Teorema das Quatro Cores: Importância Filosófica

A finalidade deste artigo é divugar um tema dentro da Filosofia da Ciência. Pretende-se abordar as questões levantadas para filosofia da Matemática pela demonstração de um dos seus teoremas clássicos, o Teorema das Quatro Cores: qual o número mínimo de cores necessárias para colorir um mapa? Procura ilustrar-se como o processo de demonstração do Teorema das Quatro Cores alterou a Matemática a nível das práticas, das técnicas utilizadas e na sua Filosofia. Não se pretende um estudo exaustivo pelo que as questões técnicas são apenas afloradas. Quer-se apenas uma introdução a temas da filosofia da Matemática de modo a que um leigo fique com noções mais sólidas.

A desconfiança e resistência à novidade ou a sua adopção e integração num património são, em última análise, parte do tema deste trabalho: o uso da informática era, nos anos 1970, o que a internet foi no início deste século e a Inteligência Artificial é atualmente.

O QUE É UM TEOREMA, QUAL A SUA UTILIDADE?

Qualquer dicionário de língua portuguesa define um teorema como sendo «qualquer proposição que, para ser admitida, precisa de demonstração». ^[1] Trata-se de um termo muito utilizado em Lógica e Matemática e que surge nos Elementos de Euclides (360-295 a.C.) com o significado de “afirmação que pode ser provada”.

Enquanto um teorema não é demonstrado recebe o nome de conjectura. A demonstração da correcção de um teorema é chamada prova. Esta relaciona logicamente premissas e conclusões. Vocábulos associados a teorema são: proposição, sentença não associada a qualquer outro teorema; lema, “pré-teorema” que serve para ajudar na prova e corolário, algo que dele decorre.

Alguns teoremas ganharam popularidade pelo seu pendor lúdico: pode-se passar o tempo a tentar demonstrar um teorema, são alguns dos populares «quebra – cabeças». Além disso, são problemas matemáticos com um grande potencial didáctico, até pela potencialidade que possuem de despertar nos jovens alunos o gosto pela descoberta e pela matemática.

Um dos teoremas mais populares devido à simplicidade da formulação é o chamado Teorema das Quatro Cores. Corresponde à possibilidade de colorir um mapa com um número mínimo de cores de maneira a que dois países contíguos (com fronteira extensa, não num só ponto) não recebam a mesma tonalidade.

UMA CONJECTURA…

Fig. 1- Francis Guthrie (1831-1899). Matemático Sul – africano que formulou a Conjectura das Quatro Cores.

O Teorema das Quatro cores surge em 1852, quando Francis Guthrie (1831-1899) (figura 1) tentava colorir um mapa de Inglaterra de forma que dois condados adjacentes não ficassem com a mesma cor. Após alguma reflexão, conjecturou que qualquer mapa plano poderia ser colorido apenas com quatro cores. Francis contactou um eminente matemático seu contemporâneo, Augustus De Morgan (1806-1871), apresentando-lhe a sua conjectura. O entusiasmo deste levou-o a divulgar a Conjectura das Quatro Cores pela comunidade matemática. O problema foi discutido e teve alguns desenvolvimentos: De Morgan procurou saber, por exemplo, se quando quatro países têm dois a dois fronteiras comuns, um deles tem de estar dentro dos outros três. Este problema continuou a ser trabalhado mas sem entrar nos círculos oficiais. ^[2]

Em Julho de 1878, Arthur Cayley (1821-1895), um jurista apaixonado pela Matemática, questionava se já existia uma solução para a Conjectura das Quatro Cores na secção de Matemática da Royal Society. Cayley publicou uma pequena análise do problema nos Proceedings of the Royal Geographical Society em 1879. Nesse ano, Alfred Bray Kempe (1849-1922), também advogado e antigo aluno de Cayley no Trinity College de Cambridge, publicou uma demonstração completa do Teorema das Quatro Cores no American Journal of Mathematics. A demonstração de Kempe foi estudada por vários matemáticos que sugeriram formas de a melhorar. Assim, em 1879, considerava-se estabelecido o Teorema das Quatro Cores. ^[3]

Todavia, em 1890, Percy John Heawood (1861-1955) provou que a demonstração de Kempe tinha um erro. Não foi capaz de obter nenhuma demonstração alternativa mas provou o Teorema das Cinco Cores: não são necessárias mais do que cinco tonalidades para colorir um mapa plano onde países de fronteira comum têm cores diferentes. Esta prova era de pequena dimensão e matematicamente simples.

Em 1880 Peter Guthrie Tait (1831 – 1901) realiza também uma demonstração, que em 1891 se descobre não estar correcta. Ambas as demonstrações tiveram valor: estabeleceram-se as cadeias de Kempe, que permitiram mostrar o Teorema das Cinco Cores e foram utilizadas na redutibilidade de configurações na prova do Teorema das Quatro Cores; Tait mostrou que o problema da coloração dos vértices de triangulações planas com quatro cores é equivalente à coloração das arestas com apenas 3 cores. ^[4]

Em 1976, com a ajuda de um IBM 360, na Universidade de Illinois, Kenneth Appel e Wolfgang Haken apresentaram uma demonstração do Teorema das Quatro Cores. John Koch também colaborou nos programas computacionais. Recorreram a mil horas de uso de um computador de alta velocidade. A prova era demasiado longa para ser verificada à mão e havia a possibilidade de o computador ter cometido um qualquer erro difícil de detectar.

Para os mais cépticos, existia sempre a possibilidade de o programa usado ter sido concebido para falsear um resultado, pois era o primeiro grande teorema a ser provado com base na informática e existia competição para demonstrar o teorema.

A demonstração de 1976 ficou também a dever-se a George David Birkhoff (1884 – 1944) e Heinrich Heesch (1906-1995) que contribuíram com ideias cruciais na obtenção da prova. O trabalho do primeiro permitiu demonstrar que a Conjectura das Quatro Cores era verdadeira para mapas com 25 regiões. A prova apresentada foi tradicional, a «papel e lápis». O segundo desenvolveu os conceitos de redutibilidade, inevitabilidade e descarregamento.

Estes conceitos técnicos podem ser sintetizados: o conjunto inevitável contém tantas regiões que qualquer mapa contém pelo menos uma delas; a configuração redutível é um arranjo de países que não pode ocorrer num contra exemplo (caso um mapa possua uma configuração redutível pode ser colorido com quatro cores); e o descarregamento é um método que prova que qualquer grafo contém um sub grafo de uma lista especificada.

A dificuldade em verificar todos os cálculos feitos na demonstração de 1976 incentivou outros matemáticos a tentarem encontrar uma prova mais simples. Este trabalho tinha mais de 80 páginas de diagramas e ainda 400 micro fichas com mais informação desenhada à mão.

Surgiu assim em, 1996, uma demonstração simplificada do Teorema das Quatro Cores, cuja formulação foi o resultado de trabalho conjunto de Neil Robertson, Paul Seymour, Daniel Sanders e Robin Thomas.

Estes matemáticos reduziram a quantidade de cálculos de modo que demonstração pudesse ser reproduzida em menos de um dia. Todavia ainda hoje não existe uma demonstração que não necessite de computadores. Isso colocava em causa a existência da prova.

DEMONSTRANDO O TEOREMA DAS QUATRO CORES

Para demonstrar o teorema há que recorrer a grafos planares. Estes são representados no plano de tal forma que as suas arestas não se cruzam. Podem ser coloridos por quatro cores de modo que vértices vizinhos não recebam a mesma. ^[5]

Se qualquer grafo planar pode ser colorido com quatro cores, então qualquer mapa plano também. Isto, pois qualquer mapa cria um grafo: a capital de um país é um vértice ligada por estrada (o arco) aos países adjacentes. Os estados são as faces resultantes do facto do plano ser dividido pelo grafo. O problema de colorir o mapa passa a ser o seguinte: colorir cada vértice do grafo de maneira que dois vértices adjacentes tenham cores diferentes. Provar o Teorema das Quatro Cores corresponde a provar que todos os mapas planos podem ser coloridos com menos de cinco tons.

O Teorema das Cinco Cores havia sido demonstrado por Kempe. Este partiu de três postulados: o mapa não contém um país isolado dentro de outro (caso do Lesoto incrustado na África do Sul), o mesmo país não possui enclaves (como a região malaia de Sarawak na ilha de Bornéu) e em cada ponto de fronteira não se encontram mais do que três vizinhos. Tudo isto era feito a partir da configuração em grafos planares. Kempe chamou a este mapa um «mapa normal». Para respeitar o primeiro postulado, Kempe fez “desaparecer” o país «enclave» introduzindo um novo país que “apaga” o vértice onde se encontram países a mais. Chama a isso «redutibilidade». O seu erro, ulteriormente descoberto por Heawood, foi pensar que a situação de um país que se encontra na confluência de cinco era redutível. ^[6]

Appel e Haken vão encontrar um outro conjunto de configurações e mostrar que todas eram redutíveis. Começaram com um algoritmo e testaram através de um programa informático a redutibilidade das configurações. Sempre que não se conseguia reduzir uma configuração, o algoritmo era modificado para conceber uma nova configuração redutível. Chegaram assim a um conjunto de 1834 configurações redutíveis, posteriormente reduzidas a 1482 configurações inevitáveis. ^[7]

No início dos anos 1980 um estudante de mestrado descobre erros no trabalho de Appel e Haken. Estes irão refutar os argumentos escrevendo um novo trabalho. Instala-se uma grande polémica, semelhante às que acompanharam o teorema ao longo da sua história. Recorde-se que houve órgãos de comunicação social que se recusaram a dar nota da demonstração de Appel e Hakken devido à polémica.

Na década de 1990, uma equipa de quatro matemáticos insatisfeitos por a demonstração anterior recorrer a computador e não poder ser totalmente verificada devido à morosidade dos cálculos, enceta uma nova demonstração.

Com um método ligeiramente diferente estes quatro matemáticos bolseiros a trabalhar na Universidade de Rutgers chegaram a um conjunto de 633 configurações redutíveis (figura 2). A ideia era verificar a prova anterior, reconstituindo-a, mas a dimensão da tarefa levou-os por outro caminho. Basearam-se em algumas proposições comuns mas acabaram por construir um novo programa de computador.

Os problemas da prova de Appel e Haken foram menorizados: o artigo final tem cerca de 40 páginas, a demonstração demorou menos de três horas e meia e os meios informáticos foram considerados comportáveis tornando «possível a outros cientistas verificar todos os passos da nossa prova, incluindo programa e dados do computador».^[8]

Fig. 2- Um conjunto de configurações (figura 1 da publicação citada de ROBERTSON et. al.).

Utilizaram a aritmética integral, que consideraram mais segura em relação aos arredondamentos. Anteciparam também a crítica de a prova não poder ser considerada uma prova tradicional, pois não pode ser humanamente verificada a compilação dos programas e a infalibilidade do hardware que na prática possuíam menor possibilidade de erro sendo feitos informaticamente do que sendo realizados tradicionalmente. Reconhecem que verificar um programa informático é mais difícil que uma prova matemática da mesma extensão. ^[9]

Repare-se que em vinte anos a informática, tanto a nível de software como a nível de hardware tinha dado um salto de gigante. Não só o computador usado nesta última demonstração era mais rápido como consideravelmente menor fisicamente e em termos de valor (custo): repare-se que o IBM 360 podia ter um disco com 100MB de capacidade, mil vezes menor que o disco do computador em que se faz este trabalho.

Assim, a reconstituição da experiência tornou-se não só mais fácil como também mais acessível. O próprio número de programadores/investigadores em informática cresceu exponencialmente, tornando mais fácil repetir e verificar cada passo da experiência.

O Teorema da Quatro Cores fascinou os matemáticos durante mais de um século mas tem pouco interesse para quem realiza mapas temáticos pois, entre outras coisas, a representação gráfica perde legibilidade como se constata através de duas das figuras do trabalho, o que contraria a «arte» de transmitir informação graficamente, uma cor teria de ser empregue com o oceano e um dos postulados corresponde ao «apagamento» dos enclaves, o que dificulta a sua aplicação em cartografia.

É utilizado amiúde em aulas práticas de Geografia do ensino básico com a finalidade de problematizar uma tarefa tão simples quanto a de colorir um mapa de Portugal ou outros. Tenta-se com isso fomentar a aprendizagem dos distritos ou concelhos e criar hábitos de raciocínio mais complexos em jovens que estão a desenvolver as suas capacidades intelectuais: existem muitos mapas em que se as cores de determinadas regiões forem colocadas antecipadamente, não é possível colorir as restantes com quatro tonalidades.

Mas para quê tanto trabalho? Porque era necessário lutar durante mais de um século para resolver um teorema matemático? Poderão perguntar os apologistas da ciência «aplicada» ou os cínicos. Para responder a essa questão basta referir que a afectação de frequências diferentes numa rede de telefone móvel; a realização de exames académicos diferentes mas de igual grau de dificuldade sobre uma mesma matéria e a resolução de um problema de Soduku, inspiram-se ou podem ser reduzidos à resolução da coloração de grafos. Os programas informáticos utilizados para estas e outras funções são descendentes do de HAPPEL e HAKKEN.

PODE-SE FALAR DE PROVA?

Tratando-se de uma demonstração não convencional até que ponto se pode falar de uma prova? Com efeito o recurso a meios informáticos pode inviabilizar a existência do teorema porquanto se pode considerar que a afirmação não foi demonstrada. Para isso temos de abordar a noção de prova.

Em filosofia considera-se que uma prova deve possuir três características principais. A primeira é ser convincente, isto é ser aceite pela comunidade científica (os pares dos demonstradores) como verosímil. Deve ser verificável, um agente racional deve poder revê-la e reconstruir a sua demonstração, avaliando-a e alcançando a mesma conclusão que os seus antecessores no processo de investigação sem margem para dúvidas. Por fim, a prova deve ser formalizável. Isto é deve ser possível traduzi-la numa linguagem formal apropriada, tornando-a objectiva. O facto de a prova ser verificável e formalizável é definitivo. Com efeito caso uma prova possa ser submetida a estas duas operações é automaticamente aceite em matemática. ^[10]

Estala aqui a polémica pois a prova de Appel e Haken não pode ser totalmente verificável. Além disso, um dos lemas mais importantes, o algoritmo usado, apela a que se tome como certos os resultados obtidos «por computador». Assim, uma parte de uma prova formal parte de uma base empírica, já que é expressa numa linguagem que não é formalizada (pelo menos em termos convencionais).

Abrem-se as portas à discussão de dois pontos: qual o estatuto das provas baseadas em trabalho de computador? Se não se pode verificar o trabalho do cientista, ultrapassámos a conjectura e temos teorema (afirmação provada) ou não?

Cumpre demonstrar que a prova de Appel e Haken pode ser aceite. Para isso terá de preencher as três características das provas. Efectivamente, a maioria da comunidade aceitou a demonstração pelo que se este obstáculo fica superado havendo resistência apenas por parte dos «matemáticos formados antes do desenvolvimento dos computadores de alta velocidade». ^[11]

Todavia a prova não era verificável em todos os passos, tal como a de 1996. Nenhum matemático verificou passo a passo o lema da redutibilidade. Também se pode objectar que o computador não fornece uma prova mas a descrição de uma prova. Pode-se apelar ao uso de computadores como um novo método de prova mas então a noção de prova teria de ser alterada para que se acomodasse o novo método ^[12]

Isso seria um precedente perigoso. Não se deveria alterar a realidade ou, neste caso um padrão de aceitação de verdade, para aceitar uma teoria, mas sim rejeitar a teoria que não consegue explicar a realidade: isto é um princípio de qualquer investigação.

Pôr em causa este princípio acarreta perigos e questões que não se sabe onde terminam, tal como demonstra TYMOCZKO através do exemplo do matemático marciano e do paralelo que faz com o jogo infantil do «rei – manda»: em última instância para aceitar uma teoria fazia-se apelo não à demonstração mas à autoridade, contrariando as ideias de demonstração/experimentação e de verificação (transparência), basilares no trabalho científico.

Estas provas por computador também não são provas formais, pois pressupõem a infalibilidade dos computadores, não tendo em conta que estes falham (quer o programa, quer a máquina): pode haver alterações do processo por vírus informático, por falhas de corrente, haver defeito do hardware ou o próprio algoritmo estar mal calculado.

Qual é então o valor do trabalho realizado por computador no contexto da justificação de um resultado matemático (neste caso a redutibilidade de uma configuração)? É, devido ao exposto, menor que o de uma prova tradicional pois assenta num conjunto complexo de factores empíricos. Estaremos preparados para confiar nas provas obtidas por computador mesmo quando não compreendemos inteiramente a forma do seu trabalho? ^[13]

Trata-se então de uma questão de boa-fé no trabalho do computador. No caso da demonstração de 1976 do Teorema das Quatro Cores, tal ocorre num caso pioneiro pelo que, como em todos os casos pioneiros de ciência o argumento de boa-fé deve ser aceite: mesmo em Direito, quando se prejudica alguém, a boa-fé do arguido serve de argumento decisivo para absolvição. Seria aceite sempre, enquanto prova, de forma reservada, enquanto facto que espera verificação(ões) definitiva(s).

Também não se pode esquecer que dado a dimensão dos dados em análise, é humanamente muito difícil proceder à verificação. Esta só sucederá usando (aguardando) evoluções técnicas decisivas que permitam a demonstração final, após verificação mais rigorosa.

De resto qualquer passo novo em ciência é provisório, sendo que há sempre um momento de debate e de contestação aos resultados. Apenas quando a maioria das objecções cai é que se aceita o novo conhecimento. Isto decorre da aceitação, do convencimento, por parte dos pares cientistas.

Desta forma, o Teorema da Quatro Cores ficou estabelecido (provisoriamente) em 1976 e ficou consolidado em 1996. Foi provado em 2005 (v. figura 3). Deixou de ser uma mera conjectura. Subsistiram todavia algumas questões por esclarecer.

Fig. 3- Um mapa político do mundo colorido com quatro cores (repare-se como o oceano fica por colorir, para permitir uma maior aproximação aos postulados do teorema).

O NOVO TEOREMA DAS QUATRO CORES

A aceitação do Teorema e das provas por computador vai criar agitação no seio da comunidade dos matemáticos. Emergem novas questões epistemológicas para as quais não existiam respostas certas. Passam a coexistir novas formas de encarar a matemática.

Ocorre uma aproximação com as ciências naturais pois são colocados em causa quatro postulados da matemática: os teoremas matemáticos são conhecidos a priori; a matemática não possui conteúdo empírico; a matemática baseia-se apenas em provas, enquanto as ciências naturais se apoiam em experiências; os teoremas matemáticos possuem um maior grau de certeza que os das ciências naturais. ^[14]

Relativamente ao primeiro postulado refere-se ao facto de serem verdades que não são demonstradas através de experiências mas pela razão. O Teorema foi demonstrado através de experiências realizadas por computador, sendo assim uma verdade a posteriori, só verificada, como foi, por outra experiência por computador vinte anos depois.

Esta posição será discutida no seio dos especialistas, mas é aquela que, por colocar problemas mais fortes foi escolhida para ser debatida aqui. A título de exemplo de um especialista que esgrime argumentos com TYMOCZKO veja-se SWART. ^[15]

Surge assim o que TYMOCZKO chama «o novo Teorema das Quatro Cores». Aceitar o teorema implica modificar o conceito de prova, de modo a que inclua as provas fornecidas por computador.

Este autor chama a atenção para o facto de Appel e Haken terem desenvolvido não uma prova mas um argumento probabilístico sobre o número de configurações redutíveis e acrescentaram-lhe o argumento de que as técnicas necessárias poderiam ser programadas informaticamente.

É assim necessário alterar novamente o conceito de prova para aceitar argumentos probabilísticos que têm a possibilidade de não estarem correctos, passando a estar sempre implícito um possível erro, o que não ocorria com as provas tradicionais, formais. Existiria assim a necessidade da matemática «formal» ter de conviver com a matemática «probabilística».

Estaria então a ocorrer na Matemática o que Khun apelida de mudança de paradigma? Tal entronca em dois obstáculos. O primeiro é a Matemática não ser encarada como uma estrutura dinâmica que se desenvolve no tempo, o que poderia ser esgrimido como estando-se em período de mudança de paradigma. O segundo obstáculo é histórico. Os paradigmas são definidos em termos de desenvolvimento passado, tendo efeitos no desenvolvimento da ciência. Uma coisa é caracterizar um acontecimento como um paradigma com base no seu registo histórico, outra é assumir que um fenómeno recente funcionará como paradigma a partir de dados limitados. ^[16]

Entretanto, em 1979 um filósofo húngaro, Imre LAKATOS (1922-1974), baseando-se numa abordagem historicista, começa a dar exemplos de provas informais que demonstram intuitivamente as suas conclusões, chama-lhes «experiências conceptuais».

De acordo com este matemático os resultados formais podem ser baseados em provas informais não formalizáveis através da teoria original: são as provas pós – formais, uma classe de provas não definida, pois são verdadeiras numa estrutura mas falsas noutra, sendo igualmente falíveis. Isso acarretaria que um teorema não seria nunca uma verdade inatacável, mas que ainda não se havia encontrado um contra-exemplo. Surgindo este, algo que não pudesse ser explicado recorrendo ao teorema, este era ajustado. Existia assim uma forma contínua de acumulação de conhecimento, através de um processo de provas e refutações. O conhecimento matemático seria baseado na heurística. ^[17]

Estaria assim a aplicar-se à Matemática a teoria de Hegel da História, do confronto entre tese e antítese surgiria uma síntese que sofreria posteriormente o mesmo processo.

Outro autor não fala de prova mas de «resultado calculado», é reconhecida uma nova forma de fazer matemática, falível, baseada na probabilidade e que recorre a técnicas de difícil verificabilidade mas que são inevitáveis para provas complexas e/ou longas no sentido em que ultrapassam a capacidade de trabalho humana. ^[18]

Os matemáticos tinham de aprender a lidar com a probabilidade e a incerteza. Tal permitiria aceitar a demonstração do Teorema das Quatro Cores mesmo sem formalizar a linguagem e não havendo verificação total dos dados.

Isto vai de encontro à forma pós – moderna de encarar o mundo, que sustenta que coexistem diversas formas de realizar a mesma coisa desde a arquitectura à matemática. De resto em Filosofia da ciência seguia o que já era sustentado por outros autores^[19].

Todavia, caso se aceitasse tacitamente a prova por computador e o relativismo inerente à probabilidade de certeza, ficava uma indefinição: quando é que se podia falar de um conhecimento estabelecido pela Matemática? Deveria esta limitar-se a refutar afirmações incorrectas sendo o património científico apenas aquilo que não se provava falso? Já não existia lugar para provas formais?

A PROVA FORMAL

A prova formal surge por um canadiano francófono perito em linguagens de programação e na verificação formal de programas informáticos. Era à altura investigador sénior da Microsoft Research Cambridge.

A resolução do teorema resume-se em poucos passos. Inicialmente reduz-se um problema de análise infinito a um problema finito de combinatória, construindo um grafo dual do mapa e fazendo apelo a um teorema da lógica proposicional. Pode-se assim construir um mapa de poliedros que respeitam a fórmula de Euler. Seguidamente, estes são transformados em mapas cúbicos em que cada vértice tem um grau (número de arestas que nele se interceptam) correspondente a três, cobrindo cada vértice com um pequeno polígono. Aprendendo com o erro de Kempe evitam-se os pentágonos e procuram-se configurações redutíveis com maior número de lados. A redutibilidade das configurações é inevitável através da aridade média. Procuram-se configurações redutíveis junto a faces cuja aridade média em mais de duas vizinhança é inferior a seis. A criação da média é feita através do descarregamento de fracções de aridades entre faces de acordo com um pequeno conjunto de padrões locais. A prova enumera todos os polígonos nessas condições. ^[20]

Esta é, em traços gerais, a descrição do trabalho deste informático. Estes passos poderiam ser verificados. A questão da formalização passará pela utilização de uma linguagem própria, a que o investigador chama Coq- Sistema de Prova Formal, baseada numa outra mais complexa. A prova será formalizada nessa linguagem e visualizada através do que o autor apelida de hiper-mapa. O Teorema das quatro cores fica assim cabalmente provado para mapas planos. Procura-se agora aplicar os seus ensinamentos para o provar a superfícies não planares.

Todo o processo é complexo e de difícil compreensão para um leigo em Matemática e programação. O que deve ficar claro é que todos os passos podem ser verificados por um programa diferente. Repare-se que as anteriores demonstrações apoiaram-se em programas próprios e que não podiam ser replicados (figura 4).

Por outro lado, e isso é fundamental numa prova formal, mostra e permite a compreensão de como a prova funciona. Surge assim uma prova formal que pacifica os últimos cépticos. Punha-se fim a um jogo que durou mais de 150 anos!

Passo 2-3

Passo 5

Passo 8

Passo 6-7

Passo 4

Passo 1

Fig. 4- A digitalização do Teorema das quatro cores no trabalho de Gonthier (figura 3 do trabalho citado).

CONCLUSÕES

As conclusões deste breve trabalho são de duas ordens. Por um lado, conclusões que se denominarão internas, ligadas à natureza da Matemática e da sua evolução; por outro lado, as externas, relativas a Ciência em geral e à forma como a disciplina científica Matemática é encarada.

Relativamente às primeiras há a referir que surgem outras formas de encarar a Matemática, baseadas, por exemplo, na intuição. Esta ganha relevo para entender os processos criativos e até explicativos que não se conseguem formalizar. Isso fica patente na discussão das novas formas de prova. Também os profissionais desta ciência se viram «obrigados» a aceitar as provas por computador sempre que estavam envolvidas grandes quantidades de dados: o que TYMOCZKO considerou polémico é aceite correntemente trinta anos depois. Isto até por uma questão de pragmatismo relativamente ao cálculo manual e à necessidade de apresentar conclusões: uma probabilidade de certeza de 99,9(9)%, pode ser considerada certeza para efeitos práticos. A evolução tecnológica mitiga as questões que se levanta(va)m. Tal como ROBERTSON e a sua equipa argumentavam, por vezes o recurso à informática vem mesmo reduzir as hipóteses de erro. Além disso, surgem também novas áreas em Matemática que só podem ser abordadas através destas técnicas.

No que toca às segundas, relativas à disciplina mas que também a extravasam, referem-se a necessidade de ponderação e discussão antes da aceitação completa de provas. Por vezes e como a história do Teorema das Quatro Cores ilustra, é necessário aceitar provisoriamente um resultado que será posteriormente, com o desenvolvimento da técnica, plenamente demonstrado.

Repare-se que caminham em conjunto máquina, programa e recursos humanos (ensino e difusão e acumulação de saber e saber – fazer). Apenas quando há uma «conjugação feliz» dos três se resolve definitivamente a questão. O Teorema das Quatro Cores contribui decisivamente para que o computador (informática) passasse a ser parte das técnicas científicas, sendo presentemente prática corrente a existência de modelos computacionais nas matemáticas aplicadas e ciências cognatas. Ocorre igualmente uma reformulação da imagem da Matemática que passa a estar mais próxima das ciências naturais, recorrendo a experiências e que aceita a relatividade do conhecimento e a falibilidade das demonstrações. Aceita igualmente provas formais e não formais, sendo uma estrutura que se desenvolve no tempo.

Esta imagem da Matemática não chegou ainda ao grande público onde a disciplina goza de uma reputação de solidez indiscutível: repare-se nas expressões populares: «demonstrar por a + b» ou «precisão matemática» quando se fala de algo cuja certeza não levanta dúvidas.

BIBLIOGRAFIA

K. APPEL; W. HAKEN; J. KOCH; Every planar map is four colorable. Part I. Discharging, ILLINOIS J. MATH., volume 21, 1977, 429-490.

K. APPEL; W. HAKEN; J. KOCH; Every planar map is four colorable. Part II.Reducibility, ILLINOIS J. MATH., volume 21, 1977, 491-567.

J. R. BROWN Philosophy of Mathematics, (Routledge 2008).

G. GONTHIER; Formal Proof-The Four Color Theorem, NOTICES OF THE AMS, Volume 55, Número 11, Dezembro 2008.

I. LAKATOS, Proofs and Refutations, (Cambridge University Press 1976).

O. ORE The four-color problem, (New York: Academic Press 1967).

N. ROBERTSON; D. P. SANDERS; P. SEYMOUR; R. THOMAS; A New Proof of the Four-Colour Theorem; ELECTRONIC RESEARCH ANNOUNCEMENTS OF THE AMERICAN MATHEMATICAL SOCIETY; Volume 2, Número 1, Agosto 1996.

THOMAS TYMOCZKO, The Four-Color Problem and Its Philosophical Significance, THE JOURNAL OF PHILOSOPHY, Vol. 76, No. 2. (Feb., 1979), pp. 57-83.

FONTES DA FIGURAS

FIGURA 1- http://upload.wikimedia.org/wikipedia/commons/5/56/Francis_guthrie.jpg

FIGURA 2- N. ROBERTSON; D. P. SANDERS; P. SEYMOUR; R. THOMAS; A New Proof of the Four-Colour Theorem; ELECTRONIC RESEARCH ANNOUNCEMENTS OF THE AMERICAN MATHEMATICAL SOCIETY; Volume 2, Número 1, Agosto 1996.

FIGURA 3- http://es.wikipedia.org/wiki/Archivo:Four_color_world_map.svg

FIGURA 4- G. GONTHIER; Formal Proof-The Four Color Theorem, NOTICES OF THE AMS, Volume 55, Número 11, Dezembro 2008.

1. J.P. MACHADO (coord.) Grande Dicionário da Língua Portuguesa, vol. XI, (Amigos do Livro Editores 1981). ↑
2. O. ORE The four-color problem, (New York: Academic Press 1967). ↑
3. Ibid. ↑
4. Op. cit. em 2. ↑
5. K. APPEL.; W HAKEN; J. KOCH; Every planar map is four colorable. Part I. Discharging, ILLINOIS J. MATH., volume 21, 1977, 429-490. ↑
6. Ibid. ↑
7. K. APPEL; W. HAKEN; J. KOCH; Every planar map is four colorable. Part II.Reducibility, ILLINOIS J. MATH., volume 21, 1977, 491-567. ↑
8. N. ROBERTSON; D. P. SANDERS; P. SEYMOUR; R. THOMAS; A New Proof of the Four-Colour Theorem; ELECTRONIC RESEARCH ANNOUNCEMENTS OF THE AMERICAN MATHEMATICAL SOCIETY; Volume 2, Número 1, Agosto 1996. ↑
9. Ibid. ↑
10. T. TYMOCZKO The Four-Color Problem and Its Philosophical Significance, The Journal of Philosophy, Vol. 76, No. 2. (Feb., 1979), pp. 57-83. ↑
11. K. APPEL; W. HAKEN; J. KOCH; Every planar map is four colorable. Part II.Reducibility, ILLINOIS J. MATH., volume 21, 1977, 491-567. ↑
12. Op. cit. em 11. ↑
13. Op. cit. em 11. ↑
14. Op. cit. em 11. ↑
15. E. R. SWART The philosophical implications of the four-color problem, AMERICAN MATHEMATICAL MONTHLY (Mathematical Association of America,1980) 87 (9): 697–702. ↑
16. Op. cit. em 11. ↑
17. I. LAKATOS, Proofs and Refutations, (Cambridge University Press 1976). ↑
18. J. R. BROWN Philosophy of Mathematics, (Routledge 2008). ↑
19. P. FEYERABEND Against Method, (Verso: 1993). ↑
20. G. GONTHIER; Formal Proof-The Four Color Theorem, NOTICES OF THE AMS, Volume 55, Número 11, Dezembro 2008. ↑