vltanh/formalizar-artigo-de-matematica

Formalizando um artigo de matemática em Lean 4

Você entrega um projeto Lean, com documentos sobre ele, em que:

• cada resultado que o artigo prova é provado pelo argumento do próprio artigo. Uma prova só se afasta da do artigo quando necessário, e cada afastamento é relatado (Regras, "Provas fiéis");
• cada resultado que o artigo cita em suas provas também é provado: no Mathlib, em outra biblioteca pública, ou em External/. Um resultado citado pode precisar de matemática que nenhuma biblioteca Lean tem ainda e que o projeto não pode razoavelmente construir. Tal resultado se torna uma hipótese nomeada de cada declaração que o utiliza, e a formalização então afirma claramente que é condicional;
• as declarações dizem o que o artigo diz, e todo desvio é documentado;
• lake build é bem-sucedido sem sorry (exceto nas declarações de Challenge.lean, por design), sem admit e sem axiom do projeto. Toda declaração da biblioteca depende apenas de propext, Classical.choice e Quot.sound;
• REPORT.md audita o artigo contra a formalização. Termina com o que vem a seguir: como o assunto se desenvolveu desde o artigo, como seus resultados poderiam ser estendidos, generalizados ou fortalecidos, e como suas provas poderiam ser mais simples. README.md resume a formalização, e CREDITS.md diz como foi feita: o procedimento, os agentes e modelos, e o tempo e esforço (o log de execução);
• um NEXT.md privado, nunca publicado a menos que o usuário peça, responde qual artigo o usuário poderia escrever a seguir seguindo este: alguns candidatos que cada um renderia um artigo próprio, explorados em profundidade (o obstáculo, as tentativas, a evidência, o que já está provado), não uma lista de extensões incrementais;
• o projeto é empacotado para Palomar e, com a permissão do usuário, publicado e executado através do pré-voo do Palomar.

O trabalho tem duas etapas. Na Etapa 1, formalize tudo o que o próprio artigo prova. Resultados que ele tira da literatura podem ser axiomas temporários. Na Etapa 2, remova esses axiomas: prove-os, ou transforme os inalcançáveis em hipóteses declaradas. A configuração vem antes das duas etapas, e verificação, limpeza, auditoria e empacotamento vêm depois.

Princípios

Estes explicam as regras abaixo. Use-os quando nenhuma regra cobrir uma situação.

• O artigo é a fonte da verdade para declarações e argumentos; Lean julga a correção. Uma declaração que difere da do artigo é uma formalização errada, por mais limpa que seja sua prova. O mesmo vale para uma prova que chega à declaração do artigo por outro argumento: a formalização verifica as provas do artigo, não apenas suas afirmações. Revise as declarações contra a fonte TeX antes que alguém as prove. Compare as provas com as do artigo depois de escritas. Nunca mude nenhuma delas silenciosamente.
• Uma formalização que ninguém compilou é um rascunho. Lean escrito de memória e nunca compilado frequentemente tem nomes de lemas adivinhados, assinaturas erradas e lemas auxiliares falsos. Compile sempre que uma toolchain Lean estiver disponível. Se não houver, ou o usuário proibir a compilação, diga claramente que o resultado não foi verificado.
• "Padrão", "óbvio", "por simetria", "rotineiro" ainda precisam de provas. Mathlib pode ter o fato; se não, prove-o. Apenas o que o próprio artigo tira de outra fonte pode se tornar um axioma.
• Externo significa de onde um resultado vem, não que é confiável. Um resultado citado vive em External/ por causa de sua fonte. É provado como todo o resto.
• Uma suposição é uma suposição, seja qual for sua forma. Um resultado citado que não é provado é assumido, quer seja escrito como um axioma, uma hipótese ou um campo de uma estrutura. Axiomas não são permitidos. Hipóteses são permitidas quando um leitor da declaração pode ver cada uma, sob o nome do resultado que ela assume. Uma estrutura que mistura dados com teoremas assumidos esconde do que um resultado depende. O mesmo vale para um parâmetro cujo tipo parece dados mas contém um teorema.
• Dados vêm com sua propriedade definidora. Quando uma declaração toma um objeto do artigo como parâmetro em vez de construí-lo, ela também deve exigir a propriedade que define o objeto. Caso contrário, o teorema é sobre todo objeto que satisfaz as outras hipóteses, o que é uma declaração diferente.
• Escolhas de representação precisam de pontes. Os objetos de Lean podem diferir dos do artigo: índices de 0 em vez de 1, listas em vez de famílias indexadas, uma estrutura Mathlib agrupada em vez de um objeto informal, um modelo concreto em vez de uma descrição "a menos de isomorfismo". Quando isso acontecer, prove um lema que conecte os dois, e documente a escolha. Nunca assuma que duas representações são equivalentes.
• Constantes e intervalos são parte da matemática. Potências, fatores, pisos, tetos, desigualdades estritas versus fracas, os pontos finais de intervalos e subtração truncada em ℕ decidem se uma declaração é verdadeira.
• Relate honestamente. Se uma etapa foi pulada, uma prova falha, uma declaração teve que mudar, ou uma prova teve que se afastar da do artigo, diga e dê a razão. A auditoria é útil apenas se puder ser confiável.
• Uma lacuna em uma prova não é uma declaração falsa. Quando a prova do artigo usa um fato que suas hipóteses não fornecem, a declaração ainda pode ser verdadeira. Procure um argumento correto antes de concluir qualquer coisa sobre a declaração.
• Meça o trabalho. Leitores e registros perguntam como uma formalização foi feita. A resposta é barata de registrar enquanto se trabalha, e difícil de reconstruir depois.

Regras

• Nunca enfraqueça ou mude a declaração de um resultado do artigo para fazer uma prova funcionar. Se a declaração do artigo for falsa, pare o trabalho nela e informe o usuário imediatamente, com o contraexemplo. Outro trabalho pode continuar enquanto isso. Se o usuário concordar, formalize a versão correta mais próxima e registre-a como um erro no relatório. Erros de digitação óbvios são a única exceção (abaixo).

• Nunca adicione uma hipótese a um resultado do artigo porque sua prova parece precisar dela. Adicionar uma enfraquece o resultado. Adicione uma apenas quando a própria declaração tiver um contraexemplo, não porque uma etapa da prova falha, e então siga a regra anterior. Caso contrário, prove a declaração como impressa, por um argumento corrigido, e registre a lacuna na prova como um item E. Se você não encontrar nem uma prova nem um contraexemplo, diga ao usuário o que está faltando. Eles decidem se continuam trabalhando ou formalizam uma declaração mais fraca, documentada como um desvio.

• Provas fiéis. Prove cada resultado pela prova do artigo: as mesmas afirmações intermediárias, as mesmas construções e divisões de caso, e os mesmos resultados anteriores onde o artigo os cita. Os resultados que a prova do artigo cita formam sua rota. A prova formal deve ter a mesma rota, e a verificação de rota (Fase 6) verifica isso. Apenas a mecânica pode diferir: táticas, o lema Mathlib que fecha uma etapa rotineira, a ordem de etapas independentes, e lemas auxiliares que empacotam uma etapa do artigo. Se Mathlib por acaso provar um resultado numerado, prove-o pelo argumento do artigo de qualquer maneira, a menos que o próprio artigo o trate como conhecido (cite-o, ou o chame de padrão).

• Afaste-se da prova do artigo apenas quando necessário, isto é, por uma destas razões e nenhuma outra:

  1. o argumento do artigo está errado naquela etapa, ou tem uma lacuna ali, e não pode ser reparado ao longo de suas próprias linhas (a etapa também é um item E);
  2. a etapa precisa de matemática que Lean não tem e que o projeto não pode razoavelmente construir (como para resultados citados fora de alcance, abaixo), e outro argumento a evita;
  3. a etapa não tem significado em uma representação que a formalização deve usar (Princípios), então uma tradução fiel dela é um argumento diferente.

  Uma prova mais curta, mais elegante, mais geral ou mais automática não é uma razão. Tampouco é uma prova mais fácil de formalizar ou mais rápida de construir. Um argumento mais simples que você encontrar ainda vale a pena guardar: registre-o, com um esboço, para a seção "O que vem a seguir" do relatório (Fase 8), e prove o resultado pelo argumento do artigo. Afaste-se tão pouco quanto a razão exigir: repare a etapa, não a prova. Se um afastamento substituiria todo o argumento de um resultado numerado, não apenas uma etapa, proponha-o ao usuário primeiro, com a razão. Outro trabalho continua enquanto isso.

• Relate todo afastamento, sempre. Para cada um, registre o que o artigo faz, o que a formalização faz em vez disso, e qual razão força a mudança. Registre-o no docstring da declaração ("Afastamento do artigo: …"), na tabela de afastamentos do relatório, em formalization.yaml (fidelity.divergences), em qualquer texto complementar, no arquivo de diferenças registradas da verificação de rota quando a rota mudar, e no próximo relatório de status. Um afastamento ausente de qualquer um destes é um defeito: encontre e corrija-o como você faria com uma declaração que foi alterada silenciosamente.

• Resultados citados fora de alcance. Um resultado citado pode precisar de matemática que nenhuma biblioteca Lean tem. Se construir essa matemática no projeto for um esforço moderado, construa-a. Caso contrário, o padrão é uma formalização condicional: o resultado se torna uma hipótese nomeada de toda declaração cuja prova o usa. Aplique o padrão sem perguntar, e relate-o no próximo relatório de status. Pergunte ao usuário apenas quando construir a matemática ausente seria um esforço grande mas factível: se gastar esse esforço é decisão deles. Enquanto isso, continue o outro trabalho sob o padrão. Se eles escolherem construí-lo, planeje o trabalho em camadas. Cada camada substitui algumas hipóteses por construções e provas a partir de outras mais básicas, e termina em um estado que pode ser lançado. Essas hipóteses são as únicas que podem ser adicionadas a um resultado do artigo sem um contraexemplo. Nunca apresente uma formalização condicional como completa: seu README, formalization.yaml e relatório dizem que é condicional e listam o que assume.

• Deslizes em declarações. Se uma declaração é falsa apenas por causa de um erro de digitação óbvio (um índice errado, um nome trocado, um - 1 faltando), e apenas uma leitura pode ser pretendida, formalize essa leitura imediatamente, na biblioteca e no Desafio. Liste cada tal correção no relatório e no próximo relatório de status ao usuário. Quando mais de uma correção for possível, trate a declaração como falsa.

• Um lema auxiliar falso (um que você ou um rascunho introduziram) precisa de um contraexemplo concreto, verificado em Lean (decide, norm_num ou #eval) quando possível. Então adicione a hipótese mínima, atualize seus chamadores, e registre a mudança na mensagem de commit.

• No final não há sorry (fora de Challenge.lean), admit, axiom, native_decide ou implemented_by. native_decide adiciona um axioma, que o Comparator rejeita.

• Nunca adivinhe um nome ou assinatura do Mathlib. Procure nas fontes fixadas em .lake/packages/mathlib, ou use #check, exact? e Loogle. Mathlib frequentemente renomeia e deprecia declarações, e avisos de depreciação nomeiam a substituição.

• Se você não puder compilar (sem toolchain, ou o usuário proibir), escreva o Lean sem compilá-lo. Verifique cada nome, assinatura e caminho de importação contra as fontes Mathlib fixadas, mantenha a ordem declarações-primeiro, e rotule cada resultado como não verificado. Quem compilar o projeto mais tarde começa na Fase 3.

• Execute um lake build de cada vez por checkout. Builds executados ao mesmo tempo deletam os arquivos .olean uns dos outros, e um editor aberto no projeto executa seus próprios builds lake setup-file. Se você vir "object file … does not exist", tente novamente em vez de editar ao redor.

• Pergunte antes de qualquer ação que outros possam ver: empurrar, criar um repositório, mudar a visibilidade de um repositório, abrir ou fechar pull requests, deletar branches, executar o pré-voo do Palomar, submeter ao Palomar, registrar. Permissão para um destes não é permissão para os outros.

• Autores são pessoas. Credite sistemas de IA no README, em CREDITS.md e na seção automation de formalization.yaml, nunca como autores ou mantenedores.

• Mantenha um log de execução desde o início (veja "Log de execução" abaixo). Relate-o em CREDITS.md, em formalization.yaml e em relatórios de status.

Fluxo de trabalho

Fase	Objetivo	Feito quando
0. Configurar	registrar a tarefa, fazer as perguntas em aberto	configuração registrada
1. Inventário	conhecer o artigo: seus resultados, definições, constantes, citações e de onde suas provas podem vir, suspeitas de erros de digitação	lista de verificação de trabalho completa
2. Projeto	um projeto Lean em uma release Mathlib, com o sistema de módulos, organizado por seção do artigo	lake build é executado
3. Declarações	toda definição e resultado numerado declarados, com provas sorry; o Desafio	declarações elaboradas e aprovam uma revisão independente contra o artigo; linha de base commitada
4. Etapa 1	provar tudo o que o artigo prova, pelas provas do artigo	apenas resultados citados permanecem, como axiomas em External/; todo afastamento relatado
5. Etapa 2	provar os resultados citados	zero axiomas; todo resultado ainda assumido é uma hipótese nomeada
6. Verificar	auditoria de axiomas, tabela de dependências, verificação de rota, Solução e Comparator	scripts/Audit.lean e a verificação de rota passam; provas comparadas com as do artigo; Comparator aceita
7. Limpeza	sem avisos, sem hipóteses não usadas, sem nomes enganosos, rotas inalteradas	o build mostra apenas os sorrys do Desafio; a verificação de rota ainda passa
8. Auditoria	REPORT.md, README.md, CREDITS.md; o NEXT.md privado	cada descoberta verificada contra a fonte TeX; cada candidato de acompanhamento verificado quanto à novidade e contra a barra
9. Empacotar	CI, arquivos e verificações Palomar; publicação e pré-voo, com permissão	as verificações locais Palomar passam; após publicação, o pré-voo relata status: pass

Commite em cada marco, com uma mensagem que diga o que mudou e por quê.

Fase 0: Configurar

Registre estes. Pergunte ao usuário apenas sobre o que você não pode resolver sozinho:

papel:            arXiv id e versão (ou DOI); fonte TeX se disponível; versão posterior se houver;
                  número de páginas; seção de agradecimentos; URLs de material suplementar
diretório:        caminho para a pasta do projeto Lean
o usuário:        nome para contato; preferência por ferramenta (editor, terminal, etc.);
                  fuso horário e horário de trabalho; se compilações são permitidas;
                  se quer receber relatórios de status; se o projeto pode ser público eventualmente;
                  se a formalização pode ser submetida ao Palomar; se o usuário escreverá o artigo
                  de acompanhamento; qualquer restrição sobre quais agentes ou modelos usar
"""

Pergunte agora:

1. Qual artigo? (arXiv id e versão, ou DOI; fonte TeX se disponível)
2. Onde o projeto Lean deve ficar?
3. Compilações são permitidas?
4. O projeto eventualmente pode se tornar público? Submetido ao Palomar?
5. Mais alguma restrição?

Fase 1: Inventário

Leia o artigo inteiro. Prepare uma lista de verificação de trabalho: seções e subseções; definições e constantes (nome, símbolo, localização); resultados numerados (teoremas, lemas, proposições, corolários, conjecturas); resultados que cada um cita (referências bibliográficas e números de resultados); suspeitas de erros de digitação e declarações suspeitas. Verifique se o artigo tem material suplementar. Se não conseguir ler o artigo inteiro de uma vez, peça ao usuário e comece enquanto isso.

Fase 2: Projeto

Configure um projeto Lean em uma release Mathlib, com o esqueleto do sistema de módulos correspondente à estrutura do artigo. Cada seção principal tem seu próprio módulo. As declarações vão em arquivos sob Mathlib/ (ou o namespace da biblioteca), nomes de arquivos em minúsculas. Os arquivos da formalização (README, CREDITS, relatório, NEXT.md, formalization.yaml, o script de auditoria) vão em um diretório scripts/ ou na raiz. O Desafio (declarações do artigo transformadas em um jogo de Solução livros abertos) vai em Challenge.lean que abre um namespace separado. O lakefile.lean aponta para o release Mathlib por hash e inclui o pacote Comparator (ou, até que exista, verificações de importação).

Execute lake build. Verifique se a árvore de dependências está completa e se todos os imports são diretos (nenhum importa através do módulo de um usuário).

Não construa a biblioteca ainda; apenas configure o projeto. Se houver um rascunho, ignore-o por enquanto.

Fase 3: Declarações

Escreva cada definição e cada resultado numerado que o artigo prova. Prove cada um com := by sorry. Escreva o Challenge.lean:

/--
Resumo: uma declaração verdadeira ou falsa tirada do artigo.
A declaração pode ser verdadeira na matemática padrão, e
o jogador deve decidir. Leia o artigo para a declaração exata.
...
-/
def desafio (afirmação : Prop) : Prop := afirmação

/-! O jogo é: para cada afirmação, decida se é verdadeira e, em caso afirmativo, prove-a.
... -/

abreviação declarações : List (String × Prop) :=
  [
    ("(1) Lemma 3.2", …),
    ...
  ]

O SCHEMA de declarações deve corresponder ao do artigo: cada entrada tem o número do resultado e a declaração exata que o artigo dá, em Prop. Se a declaração do artigo depender de uma construção que a formalização ainda não tem, adie essa entrada ou torne-a um lema separado.

Compile. Corrija erros de digitação e de importação.

Revise as declarações contra a fonte TeX. Para cada uma, verifique: o nome do resultado corresponde? O corpo corresponde? As hipóteses são exatamente as do artigo? A conclusão é exatamente a do artigo? Se não, corrija. Depois disso, faça o commit.

"""

### Fase 4: Etapa 1

Preencha as provas, seguindo as regras acima. Para cada resultado, siga a prova do artigo: construções, divisões de caso, resultados citados. Se a prova do artigo pular uma etapa, preencha-a com um lema auxiliar. Se a prova do artigo estiver errada ou tiver uma lacuna, registre-a como um item E e prossiga. Se o resultado citado for uma fonte publicada, coloque-o em `External/` com uma prova temporária `:= by sorry` e um comentário "Axioma temporário: provar na Etapa 2".

Compile após cada resultado provado, ou após cada seção.

Quando todos os resultados do artigo estiverem provados, compile novamente. Então vá para a Etapa 2.

### Fase 5: Etapa 2

Substitua cada axioma temporário por uma prova real. Se a prova estiver em Mathlib, escreva exatamente a referência. Se não estiver, prove-a você mesmo. Se a prova do resultado citado precisar de matemática que o projeto não pode construir, torne-o uma hipótese nomeada de cada declaração que o usa.

Compile. Verifique se não há mais `sorry` ou `axiom`.

### Fase 6: Verificar

Execute `scripts/Audit.lean`. Este script verifica:

- Todos os axiomas do projeto (não deve haver nenhum além de `propext`, `Classical.choice`, `Quot.sound`).
- A tabela de dependências: cada declaração depende apenas das que o artigo cita (rota).
- A verificação de rota: para cada resultado numerado, a sequência de resultados que sua prova usa corresponde à sequência na prova do artigo.
- Se o Comparator estiver disponível, execute-o.

Se alguma verificação falhar, corrija e repita.

### Fase 7: Limpeza

Remova todos os avisos de compilação (subscreva ou corrija). Remova hipóteses não usadas (adicione `_` ou torne-as parâmetros implícitos). Verifique se os nomes dos resultados são descritivos e não enganosos. Execute a verificação de rota novamente.

### Fase 8: Auditoria

Escreva `REPORT.md`: resumo do artigo; tabela de desvios (o que o artigo faz, o que a formalização faz, por quê); seção "O que vem a seguir" (extensões, generalizações, simplificações); erros encontrados no artigo (itens E); quaisquer alterações de declaração; a verificação de rota; qualquer parte condicional. Escreva `README.md`: como construir, como usar, estado (completo, condicional). Escreva `CREDITS.md`: autores humanos e sistemas de IA, log de execução.

Escreva `NEXT.md` privado: candidatos a artigo de acompanhamento, com profundidade.

### Fase 9: Empacotar

Configure CI (GitHub Actions, etc.). Adicione arquivos Palomar (`palomar.yaml`, etc.). Execute as verificações locais do Palomar. Com permissão do usuário, publique no registro Palomar e execute o pré-voo.

## Formato do log de execução

Mantenha um log de execução desde a Fase 0. Formato:

YYYY-MM-DD HH:MM TZ | Fase | Ação | Resultado | Observações

Exemplo:

2025-03-15 14:30 UTC | Fase 0 | Registrado artigo arXiv:2503.12345v1 | OK | Nenhuma pergunta em aberto 2025-03-15 15:00 UTC | Fase 1 | Inventário concluído | 5 seções, 12 resultados, 2 suspeitas de erro de digitação | Item E1: Lema 3.2: sinal trocado?

Inclua o log em `CREDITS.md` e em cada relatório de status.

## Relatórios de status

Após cada fase, ou quando o usuário pedir, envie um relatório de status:

```text
Assunto: [formalização] Status: <resumo>

Fase atual: <Fase>
Progresso: <o que foi feito desde o último relatório>
Próximo: <o que será feito a seguir>
Afastamentos: <número de afastamentos, link para a tabela>
Itens E: <número, link para a lista>
Hipóteses condicionais: <número, link para a lista>
Tempo gasto: <tempo total, tempo desde o último relatório>
Log de execução: <link>
Perguntas para o usuário: <lista de perguntas, se houver>

Palavras finais

Esta skill formaliza um artigo de matemática em Lean 4. Siga as regras e o fluxo de trabalho acima para produzir um projeto que seja fiel ao artigo, compilável e útil para a comunidade. O objetivo é tornar a formalização de matemática acessível e rigorosa, com total transparência sobre o processo.