The ultimate goal of science is mechanization. Bruno Buchberger Os leitores deste site certamente já se convenceram da importância do computador para a Matemática. Softwares como o Winplot e o Mathematica (veja a seção de softwares) produzem gráficos interativos e permitem realizar cálculos numéricos e simbólicos com impressionante flexibilidade. Contudo, a atividade matemática vai muito além da visualização de figuras e da execução de cálculos (algoritmos). Os antigos matemáticos gregos — a começar por Tales de Milleto — descobriram que fatos matemáticos inteiramente novos podiam ser extraídos de outros mais simples através de demonstrações. Desde então, o trabalho dos matemáticos tem se resumido em analisar, descobrir, definir, conjecturar e demonstrar. A única maneira de se obter certeza em Matemática é por meio de demonstrações. O emprego de demonstrações exige uma arrumação sistemática do conhecimento matemático, tal como a que já se encontra na obra Os Elementos, de Euclides (século III A.C). Esse fabuloso tratado de Geometria e Teoria dos Números apresenta um catálogo de idéias simples e fundamentais (introduzidas mediante definições) e dos fatos mais "evidentes" e básicos sobre as mesmas (os axiomas), a partir dos quais novos resultados (os teoremas) são conseguidos por meio de demonstrações. Depois de Euclides, muitos matemáticos viriam a acalentar o sonho de produzir um banco de dados "inteligente" de todo o conhecimento matemático, mas organizado principalmente para facilitar a criação de conceitos e a descoberta de resultados poderosos. Nessa direção podemos citar os estudos de Leibniz, Dedekind, Peirce, Peano e Russell. A Lógica tornou-se a ciência respeitável que é hoje devido ao reconhecimento do seu papel crucial em esforços desse jaez. Colocar o sonho desses grandes homens num ambiente assistido por computador é, indiscutivelmente, uma idéia natural e sedutora. Afinal, se podemos automatizar a geração de gráficos e cálculos simbólicos, por que não avançar para um sistema mais ambicioso que permita controlar demonstrações e deduções da maneira como o fazemos com os nossos cérebros? Obviamente, esta tarefa requer muito mais do que é oferecido por softwares matemáticos comuns. É preciso dispor, no mínimo, de uma linguagem de programação universal com excelentes capacidades tipográficas e simbólicas — como a do Mathematica, por exemplo. Infelizmente, esse sistema "sabe" muito pouco acerca de demonstrações. Das centenas de funções que possui, nenhuma foi concebida especialmente com o propósito de automatizar deduções. Por exemplo, não existe um comando nesse sistema que, aplicado a uma proposição matemática (como o Teorema de Pitágoras), nos dê de volta uma demonstração a partir de um conjunto de proposições assumidas. Por outro lado, dada a sofisticação do Mathematica, parece óbvio que podemos tentar, de alguma maneira, programá-lo para gerar um ambiente compreensivo como o que vimos discutindo. Será isto possível? Bem, foi exatamente isso que o matemático Bruno Buchberger começou a fazer por volta de 1996 com o seu  projeto . Bruno Buchberger é mais conhecido por ter introduzido o conceito de "base de Gröbner" em sua tese de doutorado de 1965, bem como o correspondente algoritmo para transformar um conjunto de polinômios numa tal base. (O termo propriamente dito seria introduzido mais tarde por Buchberger como uma homenagem ao seu orientador, Wolfgang Gröbner.) Atualmente, a maioria dos sistemas de álgebra por computador (CAS) possuem implementações do algoritmo de Buchberger. (Uma discussão detalhada deste célebre processo será dada na seção de Matemática Computacional deste site.) Cabe ressaltar que as demonstrações computadorizadas têm sido investigadas por vários grupos de pesquisadores em diferentes partes do mundo. Na verdade, o assunto possui uma longa história, com personagens bem conhecidos (como os do campo da Inteligência Artificial). Por exemplo, a página de Martin Davis (cujo link colocamos na seção História) contém um pequeno artigo (The early History of Automated Deduction) que relata os primeiros progressos da década de 1950. No entanto, o projeto é especialmente importante para a filosofia deste site pela sua fascinante combinação de conhecimentos de Lógica e Matemática em um avançado sistema de álgebra por computador como o Mathematica. O papel da Lógica, aqui, é o de fornecer as ferramentas para o tratamento formal que se faz necessário para atingir flexibilidade e precisão não só para implementação dos algoritmos, mas também para a própria comunicação com o sistema. Mais ainda, a Lógica fornece resultados teóricos importantes sobre as limitações dos processos algorítmicos (como os teoremas de Gödel). Esses assuntos serão apresentados em diferentes seções deste site, particularmente na parte devotada à Lógica Matemática. Como curiosidade, notamos desde já a presença do simbolismo lógico na logomarca do projeto de Buchner. O sinal "" denota o quantificador existencial (o "existe") e é, de fato, uma forma estilizada (sem serifas) do "E" invertido. Já o símbolo "" para o quantificador universal (o "para todo") provém de um "A" invertido. (Essas inversões de sinais são explicadas no Capítulo III do CD Números.) Portanto, "" significa "Theorema", a forma latina de "Teorema". O programa já se encontra disponível (gratuitamente) sob a forma de um pacote do Mathematica. Divulgaremos os progressos obtidos em vários artigos desta seção. Por ora, damos o ponta-pé inicial fornecendo o link abaixo para a página do , na qual podem ser encontrados cadernos do Mathematica e vários artigos relacionados ao projeto (incluindo referências às pesquisas de outros grupos). THEOREMA. A porta de entrada para este ambicioso projeto.   Carlos César de Araújo, 9 de julho de 2002 Última alteração: 16 de agostode 2009