A formalization of Borel determinacy in Lean

Este artigo apresenta uma formalização do teorema de Martin sobre a determinância dos jogos de Borel no provador de teoremas Lean 4, seguindo a prova indutiva pura de Martin.

O essencial

Imagine que o universo da matemática é como um gigantesco tabuleiro de xadrez infinito, onde dois jogadores, o "Zero" e o "Um", fazem movimentos um após o outro para sempre. O jogo nunca termina; ele gera uma sequência infinita de movimentos. A pergunta central é: existe uma estratégia vencedora para um dos jogadores? Ou seja, um dos dois pode garantir que vai ganhar, não importa o que o outro faça?

Este artigo é sobre como um matemático chamado Sven Manthe usou um computador superpoderoso (o assistente de prova Lean) para provar que, para uma classe muito específica e complexa desses jogos (chamados "Jogos de Borel"), sempre existe um vencedor.

Aqui está a explicação simplificada, usando analogias do dia a dia:

1. O Grande Desafio: O Labirinto Infinito

Pense nos "Jogos de Borel" como labirintos infinitos. A regra é que o caminho (o jogo) deve seguir certas regras de construção, como se fosse feito de blocos de Lego que podem ser combinados de formas complexas (uniões, interseções, inversões).

Na matemática tradicional, provou-se nos anos 70 que, nesses labirintos específicos, um dos jogadores sempre tem um plano infalível para vencer. Mas provar isso é como tentar montar um quebra-cabeça de 1 milhão de peças sem ver a imagem final. É tão complexo que exige uma "força" matemática enorme.

2. O Assistente de Prova: O "Chefe de Obra" Rigoroso

Sven Manthe decidiu usar o Lean, que é como um "chefe de obra" digital extremamente rigoroso.

• O que ele faz: Você não pode apenas dizer "isso é óbvio". Você tem que mostrar cada tijolo, cada cimento e cada regra de como eles se encaixam.
• O problema: O Lean é muito estrito. Ele não aceita "achismos". Se você tentar pular uma etapa, ele grita "Erro!".
• A conquista: Manthe conseguiu traduzir a prova complexa do matemático Donald Martin (que ganhou o prêmio por isso) para a linguagem que o Lean entende. Foi como traduzir um poema antigo e complexo para uma linguagem de programação moderna, sem perder nenhuma beleza ou lógica.

3. A Estratégia: "Desenrolando" o Fio

A prova original de Martin é complicada. Imagine que você tem um novelo de lã muito emaranhado (o jogo complexo). Para saber quem ganha, você precisa "desenrolar" esse novelo até que ele se torne um fio reto e simples, onde a vitória é óbvia.

• O conceito de "Desenrolar" (Unravelability): Manthe e Martin mostram que, para qualquer jogo complexo, você pode construir um "jogo espelho" mais simples. Se você ganha no jogo espelho, você ganha no jogo original.
• O desafio da contagem: O problema é que, para jogos muito complexos (com infinitas camadas), desenrolar um de cada vez é impossível. É como tentar desenrolar um novelo que cresce enquanto você o desenrola.
• A solução de Manthe: Ele usou uma ferramenta chamada Teoria das Categorias (que é como um mapa de conexões entre diferentes mundos) para lidar com a parte mais difícil: a soma infinita de jogos. Em vez de contar passo a passo, ele criou uma "máquina" que olha para todos os passos ao mesmo tempo e garante que, se cada parte funciona, o todo funciona.

4. O Dilema do "Valor Lixo" vs. "Regra Real"

Uma das partes mais interessantes do artigo é uma discussão sobre como programar regras parciais.

• A abordagem do Lean (O "Valor Lixo"): Normalmente, no mundo da computação, se uma função não tem resposta para um caso, ela joga um "lixo" (como um zero ou um valor falso) para não quebrar o sistema. É como um caixa de supermercado que, se não sabe o preço de um item, coloca "0" e segue em frente, assumindo que o cliente vai corrigir depois.
• A abordagem de Manthe (A "Regra Real"): Manthe decidiu não usar "lixo". Ele fez o Lean aceitar apenas os casos onde a regra realmente existe. É como dizer: "Se o item não tem preço, o sistema não processa a compra; ele para e pergunta o preço".
• Por que isso importa? Isso torna a prova muito mais fiel à matemática real, mas é muito mais difícil de programar. O Lean tinha que ser "ensinado" a lidar com essa rigidez. Manthe teve que criar ferramentas especiais (como um "robô de limpeza" de código) para evitar que o computador ficasse lento tentando verificar todas as regras infinitamente.

5. Por que isso é importante?

• Confiança Absoluta: Antes, tínhamos apenas a prova de um matemático humano. Agora, temos uma prova verificada bit a bit por um computador. É impossível que haja um erro de lógica escondido ali.
• O Futuro: Isso abre a porta para provar coisas ainda mais estranhas e complexas. Se conseguimos provar que jogos de Borel têm vencedores, talvez no futuro possamos provar coisas sobre o universo físico ou inteligência artificial usando a mesma lógica.
• A Lição: O artigo mostra que, mesmo que a matemática seja muito abstrata e difícil, podemos construir pontes sólidas entre ela e a computação, desde que sejamos pacientes e criativos.

Em resumo: Sven Manthe pegou um dos problemas mais difíceis da matemática moderna, traduziu-o para a linguagem de um robô superlógico, corrigiu as ferramentas do robô para que ele não usasse "atalhos sujos", e conseguiu fazer o robô confirmar que, no fim das contas, em qualquer jogo de Borel, alguém sempre tem um plano para vencer.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "A formalization of Borel determinacy in Lean", apresentado em português:

Título: Uma Formalização da Determinabilidade de Borel em Lean

Autor: Sven Manthe
Publicação: Annals of Formalized Mathematics, Vol. 2 (2026)

---

1. O Problema

O artigo aborda a formalização da Determinabilidade de Borel (Borel Determinacy) no provador de teoremas interativo Lean 4.

• Contexto Matemático: A determinabilidade de jogos infinitos de dois jogadores (jogos de Gale-Stewart) é um tópico central na Teoria Descritiva dos Conjuntos. Enquanto a determinabilidade para classes grandes de conjuntos (como analíticos) requer axiomas de grandes cardinais, a determinabilidade para conjuntos de Borel é provável no ZFC (Teoria dos Conjuntos de Zermelo-Fraenkel com o Axioma da Escolha).
• Desafio: O teorema de Martin (1975) que prova a determinabilidade de Borel é notoriamente complexo e exige uma fragmentação muito maior do ZFC do que a maioria dos teoremas comuns. Formalizar tal prova em um assistente de prova é desafiador devido à necessidade de manipular indução transfinita, limites inversos de árvores e estruturas de estratégias complexas.
• Estado da Arte: Antes deste trabalho, nenhum assistente de prova havia formalizado a determinabilidade para nenhuma classe de conjuntos além dos conjuntos fechados (closed sets).

2. Metodologia

O autor implementou uma prova baseada no trabalho de Donald A. Martin ("A purely inductive proof of Borel determinacy", 1985), com adaptações significativas para o ambiente de tipos dependentes do Lean 4.

Estrutura da Prova Formalizada:

1. Definição de Jogos:
   • Implementação de jogos de Gale-Stewart usando listas para sequências finitas e árvores (trees) para definir o espaço de jogo.
   • Definição de estratégias funcionais (funções que mapeiam posições para movimentos) em vez de "árvores de estratégia", por ser mais conveniente para a definição computacional, embora as árvores sejam usadas para conceitos de igualdade e vitória.
2. Conceito de "Desembaraçamento" (Unravelability):
   • Em vez de provar a determinabilidade diretamente por indução transfinita na hierarquia de Borel, o autor prova uma propriedade mais forte chamada Desembaraçamento Universal (Universal Unravelability).
   • Um jogo é "desembaraçável" se, para qualquer nível $k$, existe uma cobertura ($k$-covering) que transforma o conjunto de pagamento em um conjunto aberto-fechado (clopen).
   • A prova mostra que os conjuntos universalmente desembaraçáveis formam uma $\sigma$-álgebra e que jogos fechados são universalmente desembaraçáveis.
3. Construção de Limites Inversos:
   • Para lidar com uniões contáveis (um passo crucial na indução de Borel), o autor utiliza uma construção de limite inverso de jogos.
   • Abordagem Categórica: Diferente da prova original de Martin que usava indução transfinita explícita, o autor utiliza a teoria de categorias (biblioteca de matemática do Lean, mathlib) para definir o limite inverso de um sistema de árvores. Isso evita o uso explícito de ordinais e facilita a formalização da estabilização dos níveis das árvores.
4. Tratamento de Funções Parciais:
   • O autor optou por uma abordagem não convencional para o mathlib: em vez de usar "valores lixo" (junk values) para definir funções parciais (ex: definir uma estratégia para posições do oponente como 0), ele usou hipóteses proposicionais (tipos dependentes).
   • Exemplo: Uma estratégia é definida como uma função que só é válida se a posição for do jogador correto (IsPosition x p).

3. Contribuições Chave

• Primeira Formalização Completa: É a primeira vez que a determinabilidade de Borel (e não apenas de jogos fechados) é formalizada em qualquer assistente de prova.
• Adaptação da Prova de Martin: A prova segue a estrutura de Martin, mas substitui a indução transfinita por uma indução direta sobre a construção de conjuntos de Borel, introduzindo o conceito de "desembaraçamento universal" para garantir que a propriedade seja preservada sob uniões contáveis.
• Uso de Teoria de Categorias: A formalização do limite inverso de jogos utilizando a biblioteca de teoria de categorias do Lean para gerenciar morfismos e diagramas comutativos, resolvendo problemas de identificação de níveis estabilizados.
• Análise de Design de Funções Parciais: O artigo oferece uma comparação técnica detalhada entre o uso de "valores lixo" (padrão no mathlib) e o uso de tipos dependentes (hipóteses proposicionais). O autor argumenta que, para este projeto, a abordagem de tipos dependentes foi superior para a reescrita automática (rewriting), apesar de apresentar desafios de desempenho.
• Ferramentas de Automação: Desenvolvimento de táticas personalizadas para lidar com aritmética de Presburger (para verificar paridade de comprimentos de listas) e inferência de tipos para propriedades de "k-fixing" (fixação de níveis).

4. Resultados

• Código: O projeto consiste em aproximadamente 5.000 linhas de código em Lean 4.
• Prova: A prova formalizada confirma que todo jogo de Borel é determinado (ou seja, um dos dois jogadores possui uma estratégia vencedora).
• Desempenho e Limitações:
  • O uso de tipos dependentes para funções parciais causou problemas de desempenho (tempo de execução exponencial) devido à aninhamento de termos de prova.
  • O autor desenvolveu e utilizou um metaprograma (abstract / as_aux_lemma) para abstrair termos de prova em lemmas auxiliares, mitigando o problema de desempenho.
  • A prova demonstra que a força teórica necessária para a determinabilidade de Borel (que exige grandes cardinais em contextos mais fracos) é compatível com a teoria de tipos do Lean, que é equiconsistente com ZFC + cardinais inacessíveis.

5. Significado e Impacto

• Avanço na Teoria Descritiva dos Conjuntos: Este trabalho preenche uma lacuna significativa na formalização de matemática pura, trazendo um dos teoremas mais profundos da teoria dos conjuntos descritiva para o domínio da verificação formal.
• Validação da Teoria de Tipos: Demonstra que a teoria de tipos do Lean (Calculus of Inductive Constructions) é suficientemente forte para formalizar teoremas que dependem de fragmentos substanciais do ZFC, sem necessidade de axiomas extras além da consistência padrão.
• Guia para Formalização de Funções Parciais: O artigo serve como um estudo de caso importante sobre a escolha de representação de funções parciais. O autor defende que a preferência do mathlib por "valores lixo" pode ser uma desvantagem para certos tipos de raciocínio matemático (como reescrita em tipos dependentes), sugerindo que a comunidade deve reconsiderar essa convenção à medida que o suporte a tipos dependentes no Lean amadurece.
• Base Futura: O trabalho estabelece uma fundação para formalizar determinabilidade para classes de conjuntos maiores (como analíticos) sob hipóteses de grandes cardinais e para construir modelos internos a partir de axiomas de determinabilidade.

Em resumo, o artigo de Sven Manthe representa um marco na interseção entre a lógica matemática avançada e a verificação formal, provando que teoremas complexos e historicamente difíceis de formalizar podem ser tratados com sucesso através de adaptações criativas de métodos de prova e ferramentas de automação.