Estado público
Repositório de investigação e implementação
O repositório GitHub é público, mas esta página descreve um repositório de investigação e implementação, não um serviço implementado.
Voltar ao Math Lab
NPA / Verificação de provas centrada em certificados
NPA: expor o limite das evidências antes de confiar num resultado.
Esta página reconstrói a secção NPA do Math Lab como uma página autónoma de evidências: estado público, modelo de confiança, fluxo de prova, registo de afirmações, repositórios, fontes e linguagem explícita de não substituição.
- Estado público
- Repositório de investigação
- Apresentado como investigação e implementação, não como serviço de garantia em produção.
- Nova verificação pública
- 2026-07-02 / NPA v0.2.0
- Últimas etiquetas Git verificadas: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- Licença
- Apache-2.0
- Apache-2.0 foi verificada para npa, npa-std e npa-mathlib em 2026-07-02.
Verificação pública: 2026-07-02. A última etiqueta Git do repositório NPA é v0.2.0; npa-std é v0.1.0; npa-mathlib é v0.1.30. Os pinos dos README dos pacotes são apresentados como contexto específico de cada repositório e não são condensados numa única afirmação de versão do NPA.
Estado público
Indicar o que é público, o que constitui evidência e quando foi revisto.
Esta página torna visível a sua base: um instantâneo local de referência, uma fonte pública num repositório e a data da revisão final antes do lançamento.
Nova verificação pública
2026-07-02
A leitura das fontes públicas foi concluída em 2026-07-02. A reconstrução original ainda usa o instantâneo local de referência de 2026-06-21.
Evidência
Certificados e hashes
O instantâneo da fonte regista .npcert canónico, certificate_hash, export_hash, axiom_report_hash e os vereditos dos verificadores.
Licença
Apache-2.0 verificada
Apache-2.0 foi verificada para npa, npa-std e npa-mathlib através de metadados LICENSE públicos em 2026-07-02.
Limite
O NPA não é um substituto prático de Lean nem de Rocq. A simulação distribuída de inspeção no navegador não executa o próprio NPA. Etiquetas públicas, licença e visibilidade dos repositórios foram verificadas em 2026-07-02 para a revisão final antes da publicação.
Limite de confiança
Faça apenas um certificado canónico atravessar o limite das evidências.
O limite não depende de qual ferramenta parece sofisticada, mas de qual artefacto pode tornar-se evidência após verificação independente.
Parser, elaborador, táticas, automatização, pesquisa de teoremas, plugins, sistemas de IA, ficheiros-fonte, ficheiros de repetição, índices de teoremas, planos de publicação, estado de CI, páginas de versões e metadados do registo permanecem no lado não confiável dos candidatos.
Fluxo de prova / simulação explicativa
Mostrar o fluxo exato desde os bytes do certificado até às evidências de verificação.
A simulação no navegador não executa o próprio NPA, Rust, WASM nem certificados de prova reais. Ela visualiza a ordem de verificação sem código-fonte que os artefactos reais devem satisfazer.
Percurso de evidência na CLI
npa package verify-certs --root . --checker reference --json
NPA / rasto de auditoria
PRONTO
- 01 Formato do certificadobytes canónicos .npcert / certificado analisável / verificação de formato AGUARDAR
- 02 Hash do certificadobytes do certificado / certificate_hash / resumo determinístico AGUARDAR
- 03 Veredito do núcleocertificado / aceitar ou rejeitar / relatório do verificador Rust AGUARDAR
- 04 Verificador de referênciacertificado fixado por hash / aceitação ou rejeição independente / relatório do verificador sem código-fonte AGUARDAR
- 05 Relatório de axiomaspacote verificado / axiom_report_hash / inventário de pressupostos AGUARDAR
Veredito
O fluxo explicativo ainda não foi executado.Execute a explicação para marcar por ordem o percurso de verificação sem código-fonte.
Registo de afirmações
Separar as evidências, os factos sensíveis ao tempo e as afirmações de limite.
A página não depende de texto de investigação impreciso. Cada declaração pública está associada a um instantâneo local de referência, a uma fonte e a uma ação de publicação.
| Afirmação | Redação pública | Estado | Fonte | Ação de publicação |
|---|---|---|---|---|
| CL-001 | O NPA coloca o certificado em primeiro lugar: o limite auditável é o artefacto canónico .npcert e o percurso de verificação que o envolve. | Afirmação pública verificada | S01 / 2026-07-02 | Rever quando o README mudar. |
| CL-002 | A verificação pública de 2026-07-02 constatou que a etiqueta Git mais recente do repositório NPA era v0.2.0. Os README dos pacotes relacionados continuam a mostrar referências específicas de cada repositório, por isso a redação das versões permanece limitada ao respetivo repositório. | Nova verificação pública confirmada | S01 / S02 / 2026-07-02 | Manter a redação da etiqueta limitada ao respetivo repositório. |
| CL-003 | O instantâneo local de referência regista uma versão fixada da cadeia de ferramentas Rust 1.95.0; ela não é usada como afirmação de marketing. | Verificado, sensível ao tempo | S01 / 2026-07-02 | Voltar a verificar se a versão da cadeia de ferramentas for apresentada. |
| CL-004 | O NPA não é um substituto prático do Lean nem do Rocq. Este limite deve permanecer visível junto de qualquer comparação. | Afirmação de limite verificada | S01 / S03 / S05 / 2026-07-02 | Manter o aviso. |
| CL-005 | npa-std e npa-mathlib são repositórios públicos distintos de pacotes de teoremas na organização finitefield-org. | Afirmação pública verificada | S01 / S02 / 2026-07-02 | Voltar a verificar a visibilidade dos repositórios se a publicação for adiada ou se os repositórios mudarem. |
| CL-006 | Os repositórios npa, npa-std e npa-mathlib apresentam, cada um, a licença Apache-2.0 através dos respetivos metadados LICENSE públicos. | Afirmação pública verificada | S01 / S02 / 2026-07-02 | Voltar a verificar LICENSE numa versão principal. |
Repositórios e licença
Manter explícitos o código, os repositórios de pacotes e a visibilidade da organização.
As ligações aos repositórios apontam para fontes públicas, mas não garantem que esta página esteja sincronizada com o estado mais recente do GitHub.
4 repositórios apresentados
finitefield-org
npa
Cadeia de ferramentas de assistência e verificação de provas centrada em certificados.
- Licença
- Apache-2.0 verificada através de LICENSE em 2026-07-02.
- Verificação
- Última etiqueta Git: v0.2.0. Não foi publicada uma versão mais recente no GitHub. Referência atual da cadeia de ferramentas no README: NPA_GIT_TAG=v0.2.0.
experimentalRust / OCamlcentrado em certificados
Abrir repositório
finitefield-org
npa-std
Repositório do pacote padrão de teoremas para fontes de prova NPA.
- Licença
- Apache-2.0 verificada através de LICENSE em 2026-07-02.
- Verificação
- Última etiqueta Git e versão GitHub: v0.1.0. Versão dos metadados do pacote no README: 0.1.0; pino da cadeia de ferramentas do pacote: NPA_GIT_TAG=v0.1.1.
experimentalpacote de teoremasfonte de prova
Abrir repositório
finitefield-org
npa-mathlib
Repositório de investigação para uma biblioteca de matemática formal.
- Licença
- Apache-2.0 verificada através de LICENSE em 2026-07-02.
- Verificação
- Última etiqueta Git: v0.1.30. Última versão GitHub: v0.1.9. Versão dos metadados do pacote no README: 0.2.1; pino da cadeia de ferramentas do pacote: NPA_GIT_TAG=v0.1.1.
investigaçãomatemática formalbiblioteca
Abrir repositório
finitefield-org
Organização GitHub da Finite Field
Instantâneo público da organização para a família de repositórios Lab.
- Licença
- Aplicam-se licenças específicas de cada repositório
- Verificação
- npa, npa-std e npa-mathlib são públicos segundo a nova verificação da API GitHub de 2026-07-02.
índice públicoinstantâneo de visibilidadefonte
Abrir organização
Nenhum repositório corresponde à pesquisa atual.
Os repositórios GitHub são a fonte do estado público do código. Licença, etiquetas atuais, visibilidade pública e linguagem das versões foram verificados em 2026-07-02 na revisão final M10-T14.
Salvaguarda do ecossistema de provas
Clarificar as funções antes de comparar ferramentas de prova.
Esta é uma tabela de funções, não uma classificação. Lean e Rocq continuam a ser os ecossistemas de referência para assistentes de prova; o NPA é apresentado como trabalho de investigação e implementação centrado em certificados.
| Elemento | Lean | Rocq | NPA |
|---|---|---|---|
| Posição | Linguagem de programação de código aberto e assistente de prova. | Demonstrador interativo de teoremas com uma longa história de investigação. | Repositório de investigação e implementação para verificação centrada em certificados. |
| Utilização típica | Matemática, verificação de software e programação. | Matemática, especificações, verificação de programas e extração. | Investigação sobre certificados de prova, verificação independente e uma pequena base de confiança. |
| Limite da evidência | O seu próprio núcleo confiável e o ecossistema definem o limite de verificação. | O seu próprio núcleo e os desenvolvimentos verificados definem o limite de verificação. | O artefacto canónico .npcert passa da geração para a verificação. |
| Como esta página o apresenta | Referência para aprendizagem, comparação e interoperabilidade. | Referência para aprendizagem, comparação e métodos de formalização. | Projeto de investigação da Finite Field, não uma promessa de produto. |
| Limite | Continuam a ser necessários conhecimentos especializados. | Continuam a ser necessários conhecimentos especializados. | Neste momento, o NPA não é um substituto prático do Lean nem do Rocq. |
Fontes
Publicar o mapa das fontes juntamente com a interpretação.
As fontes permitem ao leitor distinguir as alegações provenientes de repositórios públicos, sites oficiais de ferramentas de prova e contexto empresarial.
S01
finitefield-org/npa
Fonte principal para o objetivo e o modelo de confiança do NPA, redação da etiqueta atual v0.2.0, comandos, estrutura do repositório e licença.
Abrir fonte S02Organização GitHub da Finite Field
Fonte principal para visibilidade pública dos repositórios, últimas etiquetas Git, páginas de versões e o instantâneo da família de repositórios Lab verificado em 2026-07-02.
Abrir fonte S03Site oficial do Lean
Fonte principal para o posicionamento público do Lean, verificada em 2026-07-02.
Abrir fonte S04Referência da linguagem Lean
Fonte principal para teoria de tipos dependentes e contexto de referência do núcleo, verificada em 2026-07-02.
Abrir fonte S05Site oficial do Rocq Prover
Fonte principal para o posicionamento público do Rocq, verificada em 2026-07-02.
Abrir fonte S06Site da empresa FINITE FIELD
Fonte empresarial para a marca Finite Field e o contexto comercial.
Abrir fonteFAQ
Estado do NPA e limites da verificação.
As respostas salientam primeiro o limite de confiança, para evitar que os leitores confundam uma página de investigação com um serviço de assistente de prova já implementado.
Conhecer a empresa01 Esta página constitui uma garantia de produto?
Não. O NPA é apresentado aqui como um repositório de investigação e implementação. Os projetos de clientes continuam a exigir requisitos próprios e critérios distintos de risco, responsabilidade e aceitação.
02 O NPA pode substituir o Lean ou o Rocq?
Não. O NPA não é um substituto prático do Lean nem do Rocq. A página mantém este limite visível porque ele é importante para definir expectativas.
03 A página executa uma verificação NPA real?
Não. A simulação no navegador não executa o próprio NPA, Rust, WASM nem certificados de prova reais. Ela explica a ordem de inspeção.
04 O que conta como evidência nesta página?
O artefacto do certificado, os hashes determinísticos, o resultado do núcleo/verificador Rust, o resultado do verificador de referência sem acesso ao código-fonte e o relatório de axiomas constituem as evidências do lado da verificação.
05 Que factos precisam de ser novamente verificados?
A versão pública atual, a visibilidade dos repositórios, as versões fixadas da cadeia de ferramentas, o texto da licença e a redação das fontes foram novamente verificados em 2026-07-02 e devem ser revistos outra vez se a publicação for adiada ou se os repositórios mudarem.
Da disciplina da prova às operações
Aplicar a mesma disciplina de evidência quando uma decisão empresarial precisa de ser fiável.
Para os sistemas empresariais, a lição útil não é acrescentar demonstração de teoremas em todo o lado. É decidir o que deve ser gerado, verificado, registado, corrigido e aprovado por pessoas.