[obm-l] Provadores automáticos de Teorema

["Ronaldo Luiz Alonso" <ronaldo.luiz.alonso@xxxxxxxxxx>]

   Muitas vezes eu me perguntei, durante muito tempo,
por que umas pessoas são mais talentosas e resolvem
problemas em matemática mais rápido que as outras
(e porque algumas pessoas como Evariste Galois
que faziam isso tinham um ego fora do comum).

   A explicação que obtinha, era que os neurônios dessas
pessoas estavam ligados de uma forma especial,
isto é, de uma forma  não trivial que facilitava a
manifestação da "ciência da não contradição"
que chamamos de matemática (isso lembra Descartes
e talvez Kant).  Tudo poderia ser esmiuçado e o
benefício da dúvida era o que construía a ciência.

    Quando li alguma coisa sobre Kurt Göedel e Bertrand
Russel entendi um pouco mais dessa ciência a partir
da metamatemática.   Porém isso não me ajudou nem
um pouco a tentar responder a questão acima.

    Mais adiante em minha vida (lá pro final da graduação)
vi alguns provadores de teorema.  Talvez o mais popular
seja o Isabelle:

http://www.cl.cam.ac.uk/Research/HVG/Isabelle/

    Quando comecei a estudar inteligência artificial naquele
ano, descobri que a "busca"  ou "árvore de busca"
parecia realmente ser a "mola mestra" daquilo
que chamamos de inteligência.  Demonstrar era
um processo de tentativa e erro.

     Mesmo assim, existiam várias estratégias de busca,
 mas apenas a "força bruta" (busca em
toda árvore) poderia
mostrar que o problema era indecidível no conjunto
de axiomas utilizado.  Mesmo nos melhores
computadores, todavia,  isso poderia
levar anos, séculos, ou talvez nunca ser conseguido
(leia por exemplo o livro "O último teorema de Fermat").


   O que sobrou de tudo isso para mim (um leigo no
assunto) foi que ela ( a matemática)
 continuou sendo a ciência da "não contradição".

        Tudo em matemática se resumia a conjuntos,
aplicações de um conjunto em outro e raciocínio lógico
usando álgebra booleana e talvez algumas fórmulas.

          Olhando por outro lado da evolução (lendo
o livro de Courant & Hilbert -Methods of Mathematical
Phisics)  vi uma redefinição
dos conceitos de integral e de continuidade
e a matemática caminhando cada vez mais para o
abstrato.

     Ao embrenhar em sistemas dinâmicos
vi que realmente a frase de Einstein começava a
se tornar verdadeira: Existia mesmo (!!) uma grande
probabilidade de alguém dominar um assunto
matemáticamente sem conhecer a sua essência.
Na época era apenas uma probabilidade.

      Daí comecei a emaranhar minha cabeça para
tendar descobrir o que causou toda essa ânsia pelo
estudo profundo das "altas matemáticas",
ou seja, que causou toda essa "coisa" que para muitos
se tornara ilegível.

  Ao pegar um livro de teoria
ergódica, por exemplo e ler o livro
me assustava terrivelmente
e achava aquilo "coisa de louco" (não era coisa
de louco... mas assustava).

       Finalmente concluí que tudo aquilo
surgiu com Newton quando ele escreveu F=ma (
na realidade ele escreveu dp/dt = F e dL/dt = T)

        Me pareceu loucura, que tudo que faziam em
matemática  avançada parecia ser resultado de F=ma!!

       Se a matemática  avançada toda vem da física,
(que em grego quer dizer natureza).  Então...  Por que
matemáticos como Hilbert queriam axiomatizá-la?
Já que as lições que aprendemos vieram todas
 da natureza?

     Não quero desencorajar ninguém, e sim
encorajar.  Estudar matemática é indispensável e
todos os que puderem devem fazer isso.

    O que não podemos é deixar de saber onde nos
encaixamos neste quebra-cabeças da
matemática moderna.
Isso nos valoriza como pessoas e nos motiva.

      Vejo muitas pessoas que fazem doutorado em
matemática, chegam a ficar em uma espécie de crise por
terem intuição acerca de um teorema, mas
não conseguirem prová-lo com rigor.  Veja:

http://www.phdcomics.com


A matemática é a ciência mais fundamental
de todas, mas assusta muita gente, sem razão.

         Assim, em termos humanos, o que seria melhor
para nós?  Usar provadores automáticos?  Eles poderiam
fazer com nossos cérebros o que o carro fez com os
nossos corações?  Vale a pena pensar?

                      O que eu digo para meus amigos
angustiados da matemática é apenas tentar acalmá-los.

         Talvez eu não sofra essa crise,
pois sou da computação, mas nunca
fui complacente com a incerteza, insegurança e dúvida
de meus amigos.

     Assim eu sempre os convido para assistir
Dumbo e tomar sorvete após vê-los estressados :)

[]s a todos.


=========================================================================
Instruções para entrar na lista, sair da lista e usar a lista em
http://www.mat.puc-rio.br/~nicolau/olimp/obm-l.html
=========================================================================