Not Letting Proofs Die: xLaDe, a Lean 4 Ecosystem Framework

No mundo da matemática moderna e da engenharia de software, há um movimento crescente para escrever provas e programas de uma forma que computadores possam verificar a correção absoluta. Em vez de depender de olhos humanos para detectar um erro em um argumento complexo, pesquisadores utilizam ferramentas de software especializadas chamadas assistentes de prova. Esses programas atuam como editores rigorosos, verificando cada passo lógico individual para garantir que um resultado seja verdadeiro além de qualquer dúvida. Sistemas como o Lean 4 tornaram-se populares para este trabalho, permitindo que grandes equipes construam bibliotecas massivas de matemática verificada e software seguro. No entanto, essas ferramentas estão constantemente sendo atualizadas e aprimoradas. Assim como uma casa construída com um conjunto de plantas pode não se sustentar se as regras de construção mudarem amanhã, uma prova matemática que funciona perfeitamente hoje pode falhar ao rodar amanhã se a versão do software mudar. Isso cria um problema para a história de longo prazo da ciência: se as ferramentas evoluírem rápido demais, o trabalho feito hoje poderá se tornar impossível de reproduzir ou compreender no futuro.

Uma equipe de pesquisadores da Universidade Central de Andhra Pradesh propôs uma nova maneira de lidar com esse desafio, não interrompendo a mudança do software, mas construindo uma camada protetora ao redor dele. Eles chamam sua criação de xLaDe, que significa Experimental Lean 4 Advanced Development Ecosystem. Em vez de tentar congelar o software Lean no tempo ou forçá-lo a permanecer o mesmo, o xLaDe atua como um sistema sofisticado de gravação e gerenciamento que se assenta sobre as ferramentas existentes. Seu objetivo é tratar o software principal como uma fundação sólida e imutável, enquanto permite que os pesquisadores experimentem livremente na superfície acima dela. O framework é projetado para capturar cada detalhe de como uma prova foi executada — a versão específica do software utilizado, as dependências e as condições exatas do ambiente — para que o trabalho possa ser reconstruído anos depois, mesmo que as ferramentas subjacentes tenham avançado.

A ideia central por trás do xLaDe é uma separação estrita entre o coração confiável do sistema e o trabalho experimental que ocorre ao seu redor. Os pesquisadores tratam o próprio software Lean como infraestrutura imutável, o que significa que ele nunca é permitido ser alterado pelos experimentos. Em vez disso, o xLaDe opera como uma camada de orquestração, um conjunto de ferramentas que envolve projetos externos sem tocar em seu código-fonte. Essa abordagem permite que cientistas testem novas ideias, mudem fluxos de trabalho e tentem diferentes maneiras de organizar seu trabalho sem arriscar a integridade das próprias provas matemáticas. Se um experimento der errado ou precisar ser descartado, ele pode ser removido de forma limpa, sem deixar uma bagunça ou afetar as partes estáveis do projeto. Essa reversibilidade é crucial, pois encoraja os pesquisadores a tentarem coisas novas sem o medo de quebrar permanentemente seu trabalho.

Para tornar este sistema utilizável, a equipe construiu uma ferramenta de linha de comando que atua como a interface principal para os usuários. Esta ferramenta gerencia diferentes "modos" de operação, permitindo que o mesmo framework sirva a diferentes necessidades. Existe um modo de integração (onboarding) para iniciantes que oferece orientação suave, um modo experimental onde pesquisadores podem testar novos fluxos de trabalho e políticas, e um modo estável que trava as coisas para um uso confiável e de longo prazo. No modo estável, o sistema impõe regras estritas para garantir que nada mude inesperadamente, tornando-o ideal para preservar resultados de pesquisa. A ferramenta também registra automaticamente metadados, como o momento em que um experimento foi executado e as versões específicas de software envolvidas, criando uma trilha de auditoria detalhada. Isso garante que qualquer pessoa olhando para o trabalho no futuro possa ver exatamente como ele foi feito e tenha as informações necessárias para repeti-lo.

Os pesquisadores testaram seu framework com dois experimentos específicos para ver se ele poderia realmente funcionar na prática. No primeiro teste, eles pegaram um pequeno projeto autossuficiente criado especificamente para o estudo e o envolveram dentro do sistema xLaDe. Eles executaram o processo de compilação do projeto através do framework sem alterar uma única linha do código original. O sistema compilou as provas com sucesso e registrou os resultados, provando que poderia gerenciar projetos externos enquanto os mantinha completamente separados do próprio framework. Em um segundo teste, mais rigoroso, eles aplicaram o mesmo método a um curso educacional completamente independente sobre Lean 4, criado por alguém fora de sua equipe. Este projeto não tinha relação prévia com o xLaDe. O framework integrou o curso com sucesso, executou seu processo de compilação e verificou que funcionava, tudo isso sem modificar os arquivos do curso ou o software Lean. Esses resultados sugerem que o sistema pode atuar como um invólucro (wrapper) universal, permitindo que diversos projetos sejam gerenciados e reproduzidos sob um conjunto comum de regras.

Segurança e confiança são centrais para o design do xLaDe. Os pesquisadores reconhecem que não podem proteger contra todas as ameaças possíveis, como um computador comprometido ou um agente interno malicioso com acesso ao código. Em vez disso, eles focam em transparência e verificação. O sistema utiliza múltiplos espelhos (mirrors) para hospedar o código, garantindo que, se um site sair do ar, o projeto permaneça acessível em outros lugares. Ele também publica chaves criptográficas e checksums, que são impressões digitais digitais que permitem aos usuários verificar se os arquivos que estão baixando são exatamente o que os autores pretendiam, sem alterações ocultas. Uma parte fundamental deste modelo de segurança é a detecção automática de qualquer tentativa de modificar o software Lean central. Se um script ou um usuário tentar alterar a fundação imutável, o sistema detecta a violação e interrompe o processo, garantindo que a integridade das provas matemáticas nunca seja comprometida pelas ferramentas experimentais.

O artigo conclui que, embora o xLaDe ainda seja um projeto experimental e não uma solução finalizada, ele oferece um caminho promissor para o futuro da verificação formal. Ele não afirma resolver o problema da compatibilidade reversa, onde códigos antigos são forçados a funcionar com novas ferramentas. Em vez disso, oferece uma solução diferente: preservar o contexto em que o código foi escrito. Ao registrar o ambiente e tratar experimentos como artefatos de pesquisa de primeira classe, o framework permite que a comunidade revisite resultados históricos com confiança. Os autores enfatizam que seu trabalho é uma metodologia para conduzir pesquisa de ecossistema, fornecendo uma maneira estruturada de testar ideias, documentar falhas e compartilhar ferramentas bem-sucedidas. Através desta abordagem, eles esperam criar um ambiente sustentável onde a rápida evolução dos assistentes de prova não ocorra à custa da perda do valioso trabalho construído sobre eles.