💻 computer science

A formalization of the Gelfond-Schneider theorem

Este artigo descreve a formalização do Sétimo Problema de Hilbert e do Teorema de Gelfond-Schneider, um resultado fundamental da teoria dos números transcendentais, utilizando o assistente de prova Lean 4.

Autores originais: Michail Karatarakis, Freek Wiedijk

Publicado 2026-03-27

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Michail Karatarakis, Freek Wiedijk

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você tem uma caixa de ferramentas matemática chamada Lean. É como um "verificador de realidade" super rigoroso que não aceita nada menos que a prova absoluta de que algo é verdade. Se você diz "2+2=4", ele pede para você mostrar cada passo, como se fosse um juiz exigente em um tribunal.

Este artigo conta a história de dois pesquisadores, Michail e Freek, que decidiram usar essa caixa de ferramentas para resolver um dos maiores mistérios da matemática: O 7º Problema de Hilbert.

Aqui está a explicação do que eles fizeram, usando analogias do dia a dia:

1. O Mistério: Números "Rebeldes" vs. Números "Organizados"

Na matemática, os números são divididos em duas grandes tribos:

Números Algébricos (Os Organizados): São números que obedecem a regras simples. Eles são raízes de equações com números inteiros. Exemplos: 2, 1/2, ou até $\sqrt{2}$ (que é a raiz quadrada de 2). Eles são "previsíveis".
Números Transcendentes (Os Rebeldes): São números que não obedecem a nenhuma dessas regras simples. Eles são caóticos e não podem ser descritos por equações normais. Exemplos famosos: $\pi$ e $e$ .

O problema de Hilbert perguntava: "Se eu pegar um número organizado (como 2) e elevá-lo a um poder que é um número 'meio-organizado' mas não inteiro (como $\sqrt{2}$ ), o resultado será um número rebelde?"

Ou seja: $2^{\sqrt{2}}$ é um número rebelde (transcendental)?

A resposta é SIM. Isso é o Teorema de Gelfond-Schneider. Mas provar isso é como tentar provar que um fantasma não existe usando apenas lógica pura. É muito difícil.

2. A Missão: Construir a "Cerca" Perfeita

Para provar que $2^{\sqrt{2}}$ é um número rebelde, os matemáticos originais (Gelfond e Schneider, em 1934) usaram uma estratégia de "cerca".

Eles imaginaram construir uma função auxiliar (vamos chamá-la de A Máquina Mágica).

O Objetivo: Criar uma máquina que, quando ligada em certos pontos, deve dar zero.
O Truque: Eles precisavam que essa máquina fosse feita de peças muito pequenas e controladas (números inteiros algébricos).
O Dilema: Se a máquina funcionar perfeitamente (dando zero onde deveria), ela deveria ser uma máquina "organizada". Mas, se ela funcionar, ela também teria que ser "pequena demais" para existir de verdade.

É como tentar construir um castelo de cartas que, ao mesmo tempo, deve ser alto o suficiente para tocar o teto, mas leve o suficiente para flutuar. É impossível.

3. O Grande Desafio: O "Verificador de Realidade" (Lean)

Aqui entra a parte genial deste artigo. Os autores não apenas fizeram a prova no papel; eles a codificaram no computador Lean.

O Lean é como um tradutor que transforma a matemática em código de computador. Se houver um único erro de lógica, o código não compila.

O Problema da "Função Mágica": Na prova original, os matemáticos usaram uma função que tinha "buracos" (pontos onde ela explodia ou não fazia sentido, chamados de singularidades). No papel, eles diziam "ignore esses buracos, vamos pular por cima".
O Problema do Lean: O computador não aceita "ignore". Se você diz "pule por cima", o Lean pergunta: "Onde você pousa? Qual é a altura exata?".
A Solução Criativa: Os autores tiveram que "consertar" a função. Eles criaram uma versão da máquina que funciona em todo lugar, preenchendo os buracos com peças de reposição perfeitas. Eles transformaram uma função "quebrada" em uma função "inteira e perfeita" (chamada de função holomorfa total). Foi como pegar um carro com buracos no pneu e soldar novas peças até que ele rodasse perfeitamente em qualquer terreno.

4. A Batalha Final: A Contradição

Depois de construir essa máquina perfeita no computador, eles fizeram o seguinte:

Lado A (Matemática Pura): Mostraram que, se o número $2^{\sqrt{2}}$ fosse "organizado" (não rebelde), a máquina teria que ser muito grande.
Lado B (Análise Complexa): Mostraram que, pelas regras da física matemática, a máquina tinha que ser muito pequena.

O computador Lean verificou cada passo e gritou: "CONTRADIÇÃO!".
Não é possível ser ao mesmo tempo muito grande e muito pequeno. Portanto, a premissa inicial estava errada. O número $2^{\sqrt{2}}$ não pode ser organizado. Ele é, necessariamente, um número rebelde (transcendental).

5. Por que isso importa?

Imagine que você está construindo uma biblioteca de fatos matemáticos que nunca podem ser errados.

Antes, tínhamos provas escritas em papel, que poderiam ter erros de digitação ou lógica falha.
Agora, temos uma prova verificada por computador. É como ter um contrato assinado pelo universo.

Isso abre portas para provar coisas ainda mais difíceis no futuro, como conjecturas sobre a natureza do universo matemático. Os autores dizem que, agora que eles aprenderam a "costurar" essas funções complexas no computador, podem tentar provar teoremas sobre curvas elípticas (usadas em criptografia de bancos) e outras áreas profundas da matemática.

Resumo em uma frase:
Dois matemáticos usaram um computador super rigoroso para provar, de uma vez por todas, que certos números misturados (como $2^{\sqrt{2}}$ ) são tão estranhos e únicos que nunca poderão ser descritos por equações simples, construindo uma "máquina matemática" perfeita para provar que eles são rebeldes.

Título: Uma Formalização do Teorema de Gelfond-Schneider

Autores: Michail Karatarakis e Freek Wiedijk (Instituto de Ciência da Computação e Informação, Universidade Radboud, Países Baixos).

1. O Problema

O artigo aborda a formalização do Sétimo Problema de Hilbert e sua solução, o Teorema de Gelfond-Schneider, no assistente de prova Lean 4 (utilizando a biblioteca mathlib).

Enunciado do Teorema: Se $\alpha$ e $\beta$ são números algébricos, com $\alpha \neq 0, 1$ e $\beta$ irracional, então $\alpha^\beta$ é um número transcendente.
Contexto: Embora a teoria dos números transcendentais tenha avançado historicamente (com Liouville, Hermite, Lindemann-Weierstrass), a prova de que números da forma $\alpha^\beta$ são transcendentais (como $2^{\sqrt{2}}$ ) exigiu métodos analíticos não elementares desenvolvidos por Gelfond e Schneider em 1934.
Lacuna na Formalização: Até este trabalho, não existia nenhuma formalização completa deste teorema em nenhum assistente de prova. Resultados anteriores focavam em constantes específicas ( $e$ , $\pi$ ) ou em teoremas mais simples (números de Liouville), mas não na estrutura geral do teorema de Gelfond-Schneider.

2. Metodologia

A prova formalizada segue a estrutura clássica de Gelfond, que envolve a construção de uma função auxiliar e a derivação de uma contradição entre limites algébricos e analíticos. A implementação no Lean 4 exigiu adaptações significativas devido à natureza construtiva e dependente dos tipos.

A. Fundamentos de Teoria dos Números Algébricos

A "Casa" (House) de um Número Algébrico: Definida como o máximo dos módulos de todos os conjugados de um número algébrico. Os autores optaram por uma definição estrutural baseada na incorporação canônica de um corpo de números $K$ em uma álgebra de Banach, em vez de usar o máximo sobre as raízes de um polinômio. Isso permitiu o uso direto da API de espaços normados do mathlib, facilitando provas de desigualdades triangulares e multiplicatividade.
Lema de Siegel para Corpos de Números: O teorema clássico de Siegel garante soluções inteiras pequenas para sistemas lineares subdeterminados sobre $\mathbb{Z}$ . Os autores generalizaram isso para o anel de inteiros algébricos $\mathcal{O}_K$ . A estratégia foi transformar o sistema sobre $\mathcal{O}_K$ em um sistema maior sobre $\mathbb{Z}$ (via representação de base), aplicar o lema clássico e "levantar" a solução de volta para $\mathcal{O}_K$ .

B. Construção da Função Auxiliar e Análise Complexa

Função Auxiliar $R(z)$ : Construída como uma combinação linear de exponenciais $R(x) = \sum \eta_i e^{\rho_i x}$ , onde os coeficientes $\eta_i$ são inteiros algébricos pequenos (garantidos pelo Lema de Siegel). A função é projetada para anular-se com alta ordem em pontos inteiros específicos.
O Desafio da Função $S(z)$ : A prova clássica utiliza uma função auxiliar global $S(z)$ $S (z)$ definida como um quociente envolvendo $R(z)$ $R (z)$ e fatores polinomiais que introduzem polos em inteiros. Em análise clássica, esses polos são evitados. No entanto, no Lean, uma definição meromorfa exigiria lidar com parcialidade (tipos de opção, subtipos) em toda a prova.
- Solução Técnica: Os autores construíram $S(z)$ como uma função total e holomorfa em todo o plano complexo. Eles utilizaram uma estratégia de "patching" (costura): definiram localmente a função removendo as singularidades (usando expansões em série de Taylor para preencher os buracos nos polos) e provaram que essas definições locais coincidem com a fórmula racional no complemento dos polos, garantindo a analiticidade global.
Limites (Bounds):
- Limite Analítico (Superior): Usando a fórmula integral de Cauchy sobre um contorno que envolve as singularidades, obtém-se um limite superior para o valor da derivada de $R(z)$ (e consequentemente para $\rho$ ) que decai exponencialmente com o aumento da ordem de anulação $r$ .
- Limite Algébrico (Inferior): Como $\rho$ é um número algébrico não nulo, seu produto de normas (sobre $\mathbb{Q}$ ) deve ser pelo menos 1. Isso fornece um limite inferior que cresce super-exponencialmente.

C. A Contradição

Ao comparar o limite superior analítico (que decai) com o limite inferior algébrico (que cresce), chega-se a uma contradição para $r$ suficientemente grande, provando que a suposição inicial ( $\alpha^\beta$ é algébrico) é falsa.

3. Contribuições Chave

Primeira Formalização Completa: É a primeira prova formal do Teorema de Gelfond-Schneider em qualquer assistente de prova.
Inovação na Análise Complexa Formal: A construção de uma função auxiliar global e totalmente analítica ( $S(z)$ ) que lida com singularidades removíveis de forma rigorosa, sem depender de definições meromorfas parciais, é uma contribuição técnica significativa para a biblioteca mathlib.
Generalização do Lema de Siegel: Implementação do Lema de Siegel para inteiros algébricos em corpos de números, essencial para a teoria de aproximação diofantina formalizada.
Rastreamento Explícito de Constantes: Diferente das provas manuais que usam notação $O(\cdot)$ , a formalização exigiu a definição e rastreamento explícito de 15 constantes ( $c_1$ a $c_{15}$ ) dependentes do grau do corpo e das propriedades geométricas, garantindo a validade da contradição final.
Aplicação Prática: O trabalho foi validado provando a transcendência da constante de Gelfond-Schneider específica: $\sqrt{2}^{\sqrt{2}}$ .

4. Resultados

O teorema foi provado no Lean 4: theorem transcendental_cpow_of_isAlgebraic_of_irrational.
O código foi integrado ao mathlib (uma biblioteca padrão de matemática formal para Lean).
A prova estabelece que para qualquer $\alpha$ algébrico ( $\neq 0, 1$ ) e $\beta$ algébrico irracional, $\alpha^\beta$ é transcendente.

5. Significado e Impacto

Marco na Teoria dos Números Transcendentais: Este trabalho move a formalização de resultados isolados (como a transcendência de $e$ ) para teoremas estruturais profundos que conectam teoria algébrica de números e análise complexa.
Base para Futuras Extensões: A estrutura desenvolvida serve como base para formalizar:
- O Teorema de Baker (formas lineares em logaritmos), que generaliza Gelfond-Schneider.
- O Teorema de Schneider-Lang (para funções meromorfas que satisfazem equações diferenciais algébricas).
- Versões p-ádicas do teorema (substituindo a análise complexa por integrais de Schnirelmann).
- Generalizações para curvas elípticas (usando a função $\wp$ de Weierstrass).
Verificação Condicional: Contribui para o esforço de verificar consequências da Conjectura de Schanuel, que ainda não foi provada, mas cujas implicações incluem o Teorema de Gelfond-Schneider.

Em resumo, o artigo demonstra a viabilidade de formalizar provas matemáticas profundas e complexas que envolvem a interação sutil entre álgebra e análise, estabelecendo novos padrões de rigor e reutilização de código na comunidade de matemática formal.