The set of primes is supernatural: a Lean formalization of the statement of the conjecture

Resumo Técnico: O Conjunto dos Primos é Sobrenatural: Uma Formalização em Lean da Enunciação da Conjectura

Enunciado do Problema
O artigo aborda a formalização da "Conjectura dos Primos Sobrenaturais", proposta originalmente em [3]. A conjectura postula que nenhuma função não constante, construída a partir da função identidade e constantes usando finitamente adições, multiplicações e potenciações pontuais, mapeia todo número inteiro positivo para um número primo. O artigo visa traduzir esta conjectura e o seu arcabouço teórico circundante para uma formalização verificada por máquina usando Lean 4 e a biblioteca Mathlib. O objetivo é estabelecer um alvo preciso, verificado pelo kernel, para a conjectura, permitindo que sistemas de raciocínio humano e automatizado tentem uma prova.

Metodologia
A formalização está contida inteiramente em um único arquivo Lean 4, SPCL.lean (aproximadamente 1200 linhas), que depende exclusivamente da Mathlib. A metodologia envolve uma tradução direta e exaustiva do artigo original [3] para Lean, garantindo que cada definição, exemplo, observação, resultado numerado e linha de tabela experimental tenha um correspondente verificado por máquina.

Componentes técnicos principais incluem:

• Estruturas de Elevação: O artigo axiomatiza as compatibilidades de adição, multiplicação e potenciação como uma "estrutura de elevação" (uma 4-upla $(E, +, \times, \wedge)$). Isso é formalizado como uma type class, e a categoria de tais estruturas é construída com leis de identidade e composição.
• Funções Naturais: Duas codificações equivalentes de "funções naturais" são implementadas:
  1. Construção de Palavras: Funções são geradas por palavras finitas sobre o alfabeto $\{A_+, A_\times, A_\wedge\}$ aplicadas ao conjunto de funções identidade e constantes.
  2. Fechamento Indutivo: Um predicado indutivo IsNatural é definido com construtores para identidade, constantes e as três operações. A equivalência entre estas duas definições é formalmente provada.
• Formulação da Conjectura: A conjectura é enunciada como uma proposição nomeada (Conjecture_2_1) do tipo Prop sem uma prova. Ela é explicitamente definida como uma hipótese em vez de um axioma ou um teorema com sorry, garantindo que a formalização não introduza novas suposições.
• Verificação Experimental: O artigo formaliza 89 resultados experimentais de [3, §4]. Estes são enunciados como teoremas afirmando a primalidade de valores específicos de funções até certo ponto e a compositividade do primeiro valor não-primo.
  • Para valores menores, as provas dependem de norm_num (avaliação computacional).
  • Para valores grandes (ex: $2^{2^6} + 93$), a formalização utiliza certificados de primalidade de Lucas. Estes são verificados via um lemma customizado lucasCert que checa as condições $a^{p-1} \equiv 1 \pmod p$ e $a^{(p-1)/q} \not\equiv 1 \pmod p$ para fatores primos $q$ de $p-1$, utilizando o tático reduce_mod_char da Mathlib.

Principais Contribuições

1. Formalização Exaustiva: O artigo fornece uma formalização completa e "livre de sorries" de todo o artigo [3]. Cada definição, lemma, proposição e linha de tabela está presente no código Lean.
2. Alvo de Conjectura Preciso: Ao enunciar a conjectura como um Prop nomeado e não provado, o trabalho cria um alvo específico e verificável para sistemas de raciocínio automatizado. A estrutura de dependência é transparente; qualquer prova da conjectura dependeria apenas das definições formalizadas e dos axiomas de Lean/Mathlib.
3. Extensão Matemática: A formalização estende a teoria de [3, Observação 3.4] ao definir uma classe mais ampla de funções, IsNaturalKnuthFactorialSub. Esta classe inclui:
   • Notação de seta de Knuth (onde o nível da seta é, por si só, uma função na classe).
   • A função fatorial.
   • Subtração truncada (sob a condição $g(n) < f(n)$).
     O artigo prova que a classe original de funções naturais se incorpora nesta classe estendida.
4. Verificação de Casos Provados: A formalização inclui provas para os casos onde a conjectura é conhecida por ser verdadeira (ex: polinômios não constantes, formas lineares-exponenciais e a função de Fermat), utilizando resultados clássicos de teoria dos números da Mathlib (ex: divisibilidade de polinômios, Pequeno Teorema de Fermat).

Resultados

• Consistência Formal: O arquivo SPCL.lean compila em aproximadamente 30 segundos. Ele depende apenas dos axiomas clássicos padrão do Lean (extensionalidade proposicional, sanidade de quociente, escolha) herdados da Mathlib.
• Tabelas Experimentais: Todas as 89 linhas das tabelas experimentais de [3] são formalizadas como teoremas. As provas para afirmações de primalidade de valores grandes são verificadas via certificados de Lucas checados pelo kernel, eliminando o risco de erros de transcrição em strings de fatoração.
• Equivalências Teóricas: A formalização prova a equivalência entre a formulação funcional da conjectura e sua reformulação set-teórica (que o conjunto dos primos é "sobrenatural", significando que contém nenhum subconjunto natural infinito).
• Consequências: Condicionalmente à conjectura, a formalização prova que o conjunto de números de Fermat compostos é infinito e que o conjunto de valores não-primos para qualquer função natural não constante é infinito.

Significância
O artigo afirma que sua principal significância reside no rigor e na completude da formalização. O trabalho transforma um "desafio difícil para qualquer tipo de inteligência" (como descrito em [3]) em um alvo preciso e verificável por máquina. Ao remover toda ambiguidade e garantir que cada passo seja checado pelo kernel do Lean, o trabalho permite que sistemas de raciocínio automatizado tentem uma prova da conjectura sem o risco de erro humano nas definições subjacentes. O artigo não pretende resolver a conjectura, mas sim fornecer a infraestrutura necessária para que uma solução possa ser validada. Também demonstra a viabilidade de formalizar conjecturas complexas de teoria dos números baseadas em experimentos dentro do ecossistema Mathlib.