Araújo, JoãoMatos, David Martins deRamires, João Jorge da Costa Vieira2022-12-142022-10-042022-12-14Ramires, 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/12729Em 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?porModelosTeoremasDemonstração automática de teoremasProver9MarcieXModelTheoremAutomated theorem provingdoctoral thesis101649150