2026-09-22T02:15:56Zhttps://repositorioaberto.uab.pt/server/oai/requestoai:repositorioaberto.uab.pt:10400.2/127292026-03-18T11:47:04Zcom_10400.2_15583com_10400.2_15395com_10400.2_15392col_10400.2_15585
Araújo, João
Matos, David Martins de
Ramires, João Jorge da Costa Vieira
2022-12-14T16:02:09Z
2022-10-04
2022-12-14
2025-10-04
Ramires, João Jorge da Costa Vieira - Bibliotecas de axiomáticas [Em linha]: conceitos e resultados para sistemas algébricos. [S.l.]: [s.n.], 2022. 1074 p.
http://hdl.handle.net/10400.2/12729
urn:tid:101649150
101649150
Em 1996, EQP, um programa de computador, resolveu o Problema de Robbins, um problema colocado nos anos 30 e que tinha derrotado alguns dos maiores algebristas do século XX. Em julho
de 2022, Enigma, uma ferramenta de inteligência arti cial aplicada à demonstração automática de
teoremas produzida por Josef Urban (Czech Technical University) no âmbito de uma bolsas do
Conselho Europeu de Investigação (ERC) que lhe foi concedida para o efeito, demonstrou autonomamente 75% dos teoremas na base de dados Mizar, um repositório contendo grande parte dos
teoremas mais comuns, nomeadamente os teoremas lecionados numa licenciatura ou mestrado de
matemática pura.
Os tempos são de grande mudança e a questão natural é esta: como podemos colocar estas ferramentas a ajudar o progresso da matemática?
A resposta que existe hoje consiste em fazer uma pergunta ao computador e ter uma resposta (como
aconteceu com o EQP e com a Enigma).
Mas será possível desenhar um programa para autonomamente descobrir nova matemática? Aqui
há um problema. Já hoje temos computadores capazes de descobrir milhões e milhões de novos
teoremas (isto é, sentenças válidas numa determinada teoria) de forma autónoma; mas qual o valor
dessa matemática e que impacto tem ou poderá ter? Como garantir que esses teoremas gerados não
são triviais, desinteressantes ou inúteis? E o que fazer com teoremas que não se compreendem? Que
impacto pode ter imenso ruído ou imensos ininteligíveis?
Têm sido avançadas diferentes propostas de resolver a questão natural colocada acima. Algumas
delas já revelaram falhar. Outras ainda estão a seguir o seu caminho. O objetivo desta tese é dar
uma resposta completamente diferente à pergunta e, como prova de conceito, gerar muitos teoremas,
novos, inteligíveis e interessantes.
De forma simples (a realidade é bastante mais complexa que a descrição que se segue), a resposta
que avançamos nesta tese é a seguinte. Vamos construir um plano em que num dos eixos temos
teorias e no outro eixo temos teoremas (ie, sentenças válidas sobre determinados objetos em determinada teoria). No início o nosso plano tem apenas alguns pontos (A, B), signi cando que na teoria
A o resultado B é verdadeiro. Por exemplo: Teoria de Grupos, É comutativo o grupo em que cada
elemento é inverso de si próprio. Agora, o programa, autonomamente veri ca se (X, B) é verdadeiro
(onde B é um teorema conhecido xo e X está a percorrer todas as teorias do nosso repositório).
Sempre que encontra uma prova para (Q, B), temos um teorema novo, que é totalmente compreensível e familiar, e que (no caso de Q generalizar A) será tão ou mais interessante que o teorema (A, B)
original. Por exemplo, ao correr o nosso programa no repositório, imediatamente surge o teorema:
Teoria de Semigrupos Inversos, É comutativo o semigrupo inverso em que cada elemento é inverso
de si próprio. Acontece que os grupos são uma pequena classe dentro dos semigrupos inversos, uma estrutura que
aparece naturalmente na geometria, e o teorema de grupos referido é dado em qualquer curso de
teoria de grupos, enquanto o teorema de semigrupos inversos aparentemente nem sequer aparece na
literatura.
De igual modo, dado o teorema (A, B), podemos procurar teoremas (A, X), em que X está a
percorrer teoremas conhecidos do repositório. No caso de se provar (A, P), teremos um teorema
famoso P, até então conhecido para a teoria T, e que agora se veri ca ocorrer na teoria A também.
Uma vez mais o resultado é familiar, inteligível e novo.
Um utilizador que descobre um teorema T numa axiomática A, pode colocar T no nosso sistema que
irá procurar pares (X, T), quando X percorre a base de dados de axiomáticas do nosso repositório.
Tendo como resposta (A1, T), (A2, T),..., (An, T), o utilizador cará assim a saber que o seu teorema
é um fenómeno muito mais geral e portanto pode procurar uma teoria geral Γ que contenha todas as
teorias Ai como casos particulares e na qual o seu teorema T ainda seja verdadeiro. Mais interessante
ainda, esta busca da teoria Γ pode ser feita autonomamente pelo computador.
De forma análoga, um matemático pode ser levado à introdução de uma nova classe A. O nosso
sistema vai procurar pares (A, X), onde X são teoremas na base de dados, pelo que poucos minutos
depois de ter identi cado a nova classe, o utilizador poderá já ter vários teoremas familiares, possivelmente não triviais e uma base muito mais sólida para prosseguir a sua investigação. Quando antes
a introdução de uma nova classe signi cava o início de um longo e penoso caminho a provar novos
teoremas, a início elementares, e depois crescentemente complexos, o nosso sistema permite obter
um corpo signi cativo de teoremas, podendo alguns ter provas altamente complexas, não obstante
soando familiares e compreensíveis.
É esta a resposta que esta tese propõe para a pergunta mais natural do momento: como se pode
domar, tornar signi cativa e útil, a capacidade ilimitada de gerar novos teoremas dos computadores?
In 1996, EQP, a computer program, solved the Robbins Problem, a problem posed in the 1930s and
that had defeated some of the top algebristas of the 20th century. In July 2022, Enigma, an arti cial
intelligence tool applied to the automatic demonstration of theorems produced by Josef Urban (Czech
Technical University) as part of a European Research Council (ERC) scholarship granted to him
to this end, demonstrated autonomously 75% of the theorems in the Mizar database, a repository
containing much of the most common theorems, namely the theorems taught in a bachelors degree
or masters degree in pure mathematics.
The times are of great change and the natural question is this: how can we put these tools to help
the progress of mathematics?
The answer that exists today is to ask a question to the computer and have an answer (as happened
with EQP and Enigma).
But it will be possible to design a program to autonomously discover new mathematics? Theres a
problem here. Today we have already computers capable of discovering millions and millions of new
theorems (i.e. sentences valid in a theory) autonomously; but whats the value of this mathematics
and what impact will it have? How to ensure that these generated theorems are not trivial, uninteresting or useless? And what to do with theorems we do not understand? What impact can have a
lot of trivial or deeply unintelligible statements?
Di erent proposals have been put forward to address this natural issue. Some of them already failed.
Others are still following their way. The purpose of this thesis is to give a completely di erent answer
to this main problem and, as proof of concept, generate many theorems that are new, intelligible
and interesting.
The answer we have advanced in this thesis is as follows. Lets build a plane where in one of the axes
we have theories and on the other axis we have theorems (i.e., valid sentences on certain objects in
a given theory). At the beginning our plane has only a few points (A, B), meaning that in theory
A result B is true. For example: A is Theory of Groups, and B is The group in which each element
is inverse of itself is commutative. Now the program autonomously checks whether (X, B) is true
(where B is a xed known theorem and X is going through all the theories of our repository).
Whenever you nd a proof for (Q, B), we have a new theorem, which is totally understandable
and familiar, and that (in the case of Q generalizing A or Q not related to A) will be as much
or more interesting than the original theorem (A, B). For example, when running our program
in the repository, it immediately appears the theorem: Q is Theory of Inverse Semigroups, It is
commutative the inverse semigroup where each element is inverse of itself.
It turns out that groups are a small class within the inverse semigroups, a structure that appears
naturally in geometry, and the group theory theorem referred to above is taught in any course of group theory, while the inverse semigroup theorem apparently does not even appear in the literature.
Similarly, we can look for theorems (A, X), where X is going through our repository of theorems.
In the case we get a proof for (A, P), we will have a famous P theorem, until then known for the
Theory T (the starting point was (T, P)), and that now happens to hold for theory A as well. Once
again, the result is familiar, intelligible and new.
The rst approach will give all theories in which a given result B is true; the second approach will
give all results that hold in a given theory A.
If a mathematician discovers a theorem P in an axiomatic T, then P can be added to our system
that will look for pairs (X, P), when X spans our library of mathematical theories. With the answer
(A1, P),(A2, P), ...,(An, P), the user will thus know that his or her theorem is a much more general
phenomenon and therefore can look for a general theory Γ that contains all Ai theories as particular
cases and in which theorem P still holds. Even more interestingly, this search for theory Γ can be
done independently by the computer.
Analogously, a mathematician can be led to the introduction of a new class A. Our system will
look for pairs (A, X), where X are theorems in the database, so a few minutes after identifying the
new class, the user may already have several familiar theorems, and possibly a much stronger basis
for further research. When, in the old days, the introduction of a new class meant the beginning
of a long and often painful path to prove new elementary theorems at rst, and then increasingly
complex, our system allows us to obtain upfront a signi cant body of theorems, some of which may
have highly complex proofs, but all of them will sound familiar and understandable.
This is the answer that this thesis proposes to the most natural question of the moment: how can
you control, tame, make meaningful and useful, the unlimited capacity to generate new computer
theorems?
por
Modelos
Teoremas
Demonstração automática de teoremas
Prover9
MarcieX
Model
Theorem
Automated theorem proving
Bibliotecas de axiomáticas: conceitos e resultados para sistemas algébricos
doctoral thesis
Tese de Doutoramento em Álgebra Computacional em associação com a Faculdade de Ciências e Tecnologia da Universidade de Coimbra, apresentada à Universidade Aberta
Publication
04:Educação de Qualidade
09:Indústria, Inovação e Infraestruturas
opendAccess
doctoralThesisopen.access