01 / Limite
Manter pequena a base confiável
Não coloque geradores complexos nem IA no centro da confiança. Torne explícito o pequeno lado da verificação.
Finite Field / Math Lab
Construa evidência de correção, não apenas resultados rápidos.
O Math Lab mostra como tratamos modelação matemática, demonstração de teoremas, verificação formal, reprodutibilidade e implementação confiável sem exagerar a evidência.
- Projetos públicos
- NPA / STD / MATHLIB
- Linguagem principal
- Rust
- Instantâneo do NPA
- v0.1.1
Auditoria de provas / visão conceptual
Só leitura
01 bytes canónicos / formato OK
02 certificate_hash OK
03 verificação de provas dependentes OK
04 veredito sem fonte OK
Limite de confiança visível
Esta página não afirma que o NPA seja um substituto prático de Lean ou Rocq, e a simulação no navegador não executa NPA.
Princípio do laboratório
Publique não apenas resultados, mas também o limite da verificação.
Uma conclusão como “funcionou”, “foi rápido” ou “foi provado” não basta. Mostramos separadamente entradas, pressupostos, partes confiáveis, artefactos verificáveis de forma independente e questões por resolver.
02 / Evidência
Transformar evidência em artefacto
Deixe certificados, hashes, listas de pressupostos, condições de benchmark e logs numa forma que outras pessoas possam inspecionar.
03 / Reproduzir
Desenhar para reprodutibilidade
Fixe cadeias de ferramentas, dados de entrada, comandos de execução e critérios para que o resultado possa ser verificado novamente.
04 / Honestidade
Não exagerar o estado da investigação
Mostre métodos práticos, experimentos e investigação separadamente. Coloque limitações ao lado dos resultados.
REVISÃO DE MÉTODO
Categoria de método de serviço que ainda exige âmbito, responsabilidade, evidência do cliente e aprovação antes de ser descrita como pronta para projeto.
EXPERIMENTAL
Existe uma implementação funcional, mas escala, compatibilidade, desempenho ou especificação ainda podem mudar. Versão e passos de reprodução são necessários.
INVESTIGAÇÃO
Desenho, avaliação, prova ou implementação estão em curso. Isto não implica disponibilidade comercial nem conclusão.
Portefólio de investigação
Ver investigação por maturidade e artefactos.
Cada cartão mostra maturidade, artefactos, estado atual e próxima validação. A pesquisa e os filtros usam apenas estado do navegador.
8 apresentados
EXPERIMENTAL
CÓDIGO ABERTO
01
Nano Proof Auditor
Cadeia de ferramentas de prova centrada em certificados
Cadeia de ferramentas de investigação que coloca certificados de prova canónicos e uma base pequena de verificação no centro da revisão de provas dependentes.
- Artefactos
- fonte / especificação / modelos de CI
- Atual
- instantâneo público v0.1.1
- Próxima validação
- pacotes externos de teoremas e verificação independente
EXPERIMENTAL
CÓDIGO ABERTO
02
Biblioteca Padrão NPA
Lógica / Nat / Lista / Álgebra
Repositório de pacotes de teoremas padrão para fundamentos reutilizáveis do NPA.
- Artefactos
- fonte / pacotes de prova
- Atual
- repositório público separado
- Próxima validação
- âmbito do pacote e compatibilidade
INVESTIGAÇÃO
CÓDIGO ABERTO
03
Biblioteca Matemática NPA
Biblioteca de matemática formal
Direção de biblioteca para armazenar teoremas matemáticos como pacotes de prova verificáveis de forma independente.
- Artefactos
- fonte / pacotes de prova
- Atual
- repositório público em desenvolvimento
- Próxima validação
- estrutura da biblioteca e auditoria de dependências
REVISÃO DE MÉTODO
MÉTODO
04
Modelos de planeamento com restrições
Programação / Roteamento / Alocação
Método para separar restrições rígidas e métricas de avaliação em turnos, visitas, roteamento, produção e alocação.
- Artefactos
- modelo / protótipo / relatório explicativo
- Atual
- método de serviço; afirmação pública limitada à revisão de método
- Próxima validação
- evidência do cliente e aprovação de âmbito
INVESTIGAÇÃO
MEDIÇÃO
05
Avaliação reprodutível de solvers
Benchmark e evidência
Programa para fixar conjuntos de instâncias, hardware, limites de tempo, sementes aleatórias e logs brutos antes de fazer afirmações de desempenho.
- Artefactos
- registo de benchmark / logs brutos / relatório
- Atual
- desenho do programa de investigação
- Próxima validação
- primeiro corpus público de benchmark
INVESTIGAÇÃO
MÉTODOS FORMAIS
06
Verificação de lógica empresarial crítica
Invariantes para sistemas empresariais
Investigação sobre separar taxas, permissões, inventário e transições de estado em especificações e invariantes.
- Artefactos
- especificação / invariantes / relatório de teste ou prova
- Atual
- estudo de âmbito
- Próxima validação
- selecionar um caso limitado semelhante à produção
EXPERIMENTAL
ENGENHARIA
07
Componentes confiáveis pequenos em Rust
Componentes confiáveis pequenos
Trabalho de implementação que mantém peças críticas de confiança, como verificadores e hashes, pequenas o suficiente para inspeção.
- Artefactos
- núcleo NPA / crate de certificados / verificador de referência
- Atual
- implementação pública no NPA
- Próxima validação
- compatibilidade do verificador independente
INVESTIGAÇÃO
IA × PROVA
08
Assistência de IA e verificação independente
Gerar livremente, verificar rigorosamente
Direção de investigação que coloca a IA na geração de candidatos enquanto a evidência final é verificada de forma independente.
- Artefactos
- gerador de candidatos / certificado / relatório do verificador
- Atual
- direção de investigação consistente com o modelo de confiança do NPA
- Próxima validação
- fluxo de autoria medido
Nenhuma área de investigação correspondente foi encontrada.
Experimente outra palavra-chave ou volte o filtro de maturidade para todos.
Nano Proof Auditor
Separe a geração de provas daquilo em que confiamos.
O NPA é uma cadeia de ferramentas de prova centrada em certificados para provas dependentes. Interfaces, táticas, pesquisa de teoremas, plugins, IA, ficheiros-fonte e estado de CI podem ajudar a criar candidatos, mas não são a evidência de prova confiável.
EXPERIMENTALCÓDIGO ABERTOAPACHE-2.0
Instantâneo atual
v0.1.1
Informação pública verificada em 2026-06-21.
Núcleo principal
Rust
O verificador e o núcleo Rust fazem parte do lado da verificação.
Artefacto de auditoria
.npcert
Os bytes canónicos do certificado são o objeto a inspecionar.
Ponto de reverificação
revisão manual
O estado do repositório e a visibilidade do pacote devem ser revistos antes da publicação.
Explorador do limite de confiança
Percorra o que é confiável e o que não é.
Clique em cada nó para inspecionar o que faz, o que produz e qual verificação ainda é necessária.
NÃO CONFIÁVEL
VERIFICADO
Limite importante
Atualmente, o NPA não é um substituto prático de Lean ou Rocq. Esta página explica um desenho de investigação centrado em certificados e não garante sistemas comerciais sem erros nem resolução automática de teoremas.
Verificação de certificado / simulação explicativa
Experimente o fluxo de verificação de certificados.
A interação no navegador explica o fluxo de inspeção. Ela não executa NPA, Rust, WASM nem certificados de prova reais.
Exemplo de CLI
npa package verify-certs --root . --checker reference --json
NPA / rasto de auditoria
PRONTO
- 01 Ler o certificadobytes canónicos / formato AGUARDAR
- 02 Verificar o hash do certificadocertificate_hash AGUARDAR
- 03 Verificar com o núcleoverificação de provas dependentes AGUARDAR
- 04 Reverificar com o verificador de referênciaveredito sem fonte AGUARDAR
- 05 Comparar o relatório de axiomashash do relatório de axiomas AGUARDAR
Veredito
A explicação ainda não foi executada.Execute a explicação para visualizar os passos em ordem.
Ecossistema de provas
Clarificar papéis em vez de classificar ferramentas.
Lean e Rocq são ecossistemas maduros de assistentes de prova. O NPA é apresentado aqui como um projeto de investigação e implementação centrado em certificados, não como uma classificação de substitutos.
| Item | 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. |
| Uso típico | 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 e verificação independente. |
| Ênfase | Extensibilidade, bibliotecas e demonstração interativa. | Expressividade, métodos maduros e bibliotecas. | Base confiável pequena e certificados canónicos. |
| 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. |
| Limite | Conhecimento especializado continua a ser necessário. | Conhecimento especializado continua a ser necessário. | Neste momento, não se destina a ser um substituto prático de Lean ou Rocq. |
Método de investigação
Transforme “funcionou” num procedimento de verificação repetível.
Um resultado torna-se mais forte quando alguém pode executá-lo novamente, inspecioná-lo e rejeitá-lo nas mesmas condições.
Pergunta
Defina o que deve ser verificado: desempenho, correção, compatibilidade ou âmbito.
Pressupostos
Registe pressupostos, exclusões, axiomas, lacunas de dados e vieses antes da avaliação.
Artefacto
Guarde fonte, certificados, entradas, logs de execução e hashes.
Verificação independente
Verifique resultados por um caminho diferente do lado da geração.
Benchmark
Fixe hardware, versões, limites de tempo, conjuntos de instâncias e sementes aleatórias.
Limites
Publique falhas, casos não suportados, limites de desempenho e a próxima validação.
Construtor de reprodutibilidade
Verifique o que ainda falta numa publicação de investigação.
A lista de verificação é processada apenas no navegador. Não é uma pontuação de certificação.
Prontidão
0%Próxima ação
Defina primeiro a pergunta de investigação e a condição de sucesso.Antes de decidir formatos de artefactos, fixe o que será comparado ou verificado.
Artefactos públicos
Acompanhar artefactos públicos a partir de uma entrada.
A página evita chamadas à API do GitHub em tempo de execução. O estado dos repositórios é um instantâneo revisto que deve ser verificado antes da publicação.
4 artefactos
finitefield-org
npa
cadeia de ferramentas de prova centrada em certificados
VERIFICAR
package verify-certs
finitefield-org
npa-std
pacote de teoremas padrão
FUNÇÃO
Std.Logic / Nat / List
finitefield-org
npa-mathlib
biblioteca de matemática formal
FUNÇÃO
pacotes de teoremas formais
GitHub
finitefield-org
índice de repositórios públicos
ÍNDICE
todos os repositórios públicos
Nenhum artefacto público corresponde à pesquisa.
Política de publicação
Repositórios públicos, notas de investigação e benchmarks devem indicar data de verificação, maturidade, passos de reprodução e limitações conhecidas. Estrelas e contagens de commits não são apresentadas como sinais de qualidade de investigação.
Do laboratório às operações
Leve a disciplina de investigação ao desenho de sistemas empresariais.
Nem todo o sistema de cliente precisa de demonstração de teoremas. A transferência útil está em decidir o que deve ser confiado, comparado, verificado, corrigido e aprovado por pessoas.
Prática de laboratório
Separe geração, cálculo e verificação final, em vez de confiar igualmente em todas as camadas.
Guarde entradas, saídas, certificados, hashes e logs como artefactos passíveis de revisão.
Fixe dados, versões, comandos e critérios de avaliação antes de comparar resultados.
Publique restrições, casos falhados e pontos por resolver com o mesmo peso dos resultados.
Sistema do cliente
Defina quem insere dados, quem revê, quem sobrescreve e quem confirma o resultado.
Mostre restrições, pontuações de avaliação, candidatos rejeitados e pontos por resolver.
Preserve alterações de condições, execuções de cálculo e histórico da aprovação final.
Faça com que a saída automatizada possa ser corrigida, rejeitada e explicada aos operadores.
01
Turnos e planeamento de equipa
Mostre violações de regras e atendimento de preferências separadamente.
02 Roteamento de veículosMantenha visíveis os motivos das rotas, a capacidade, as janelas de tempo e as exceções.
03 Programação da produçãoExplique trabalho não programado, gargalos e trade-offs de preparação.
04 Correspondência de alocaçõesMostre os motivos dos candidatos e as alternativas antes da aprovação.
Notas de investigação
Mantenha legíveis o histórico de atualizações e a evidência.
Nem todo o cartão é um artigo publicado. Notas em preparação continuam sem rótulo de publicação até receberem datas, fontes e passos de reprodução.
NPA / atual
Por que colocar certificados no centro
Por que a evidência final deve ser um certificado padronizado verificado por um pequeno caminho independente.
Ver repositório públicoNota de desenho / planeada
Tornar explicáveis os resultados de otimização
Nota de desenho sobre expor objetivos, restrições rígidas, preferências flexíveis e alocações por resolver na UI.
Ver demonstrações relacionadasBenchmark / planeado
Condições para comparação justa de solvers
Nota planeada sobre conjuntos de instâncias, limites de tempo, lacunas de otimalidade, sementes aleatórias e hardware.
Ver critérios de publicaçãoItens “em preparação” não são artigos publicados. Após a publicação, cada nota recebe data, fonte, autor, caminho de reprodução e limitações conhecidas.
FAQ
Limites entre investigação, ferramentas de prova e uso empresarial.
Estes pontos são explicitados antes que páginas de investigação sejam confundidas com garantias de produção.
Conhecer a empresa01 O Math Lab é um serviço de desenvolvimento contratado?
Não. É um lugar para publicar postura de investigação e artefactos. Nas conversas com clientes, separamos métodos aplicáveis, métodos que precisam de mais validação e temas ainda em fase de investigação.
02 O NPA pode substituir Lean ou Rocq?
Não. O NPA atual não é um substituto prático de Lean ou Rocq. É um projeto de investigação e implementação em torno de certificados, verificação independente e uma base confiável pequena.
03 Confiam em provas geradas por IA tal como estão?
Não. IA, pesquisa e táticas ajudam a gerar candidatos. O foco está em saber se o certificado final é aceite por um verificador independente desses caminhos de geração.
04 A verificação formal elimina todos os erros?
Não. Métodos formais verificam propriedades específicas contra uma especificação explícita. Especificações incorretas, código fora de âmbito, operações e serviços externos ainda precisam de revisão separada.
05 Isto está relacionado com trabalho em sistemas empresariais?
Sim. Normalmente aplicamos esta disciplina gradualmente: restrições, motivos dos resultados, histórico de cálculos, limites de permissões e verificações da lógica empresarial importante.
Discutir um problema
Pode discutir o trabalho a resolver, não apenas o tema de investigação.
Comece pela folha de cálculo atual, pelas regras e pelos pontos em que as pessoas corrigem decisões. Podemos organizar se modelação matemática, automação de regras ou um protótipo deve vir primeiro.
Instantâneo das fontes / 2026-06-21
As afirmações sobre o NPA baseiam-se no instantâneo do repositório finitefield-org/npa. O posicionamento de Lean e Rocq baseia-se nos seus sites oficiais. O estado dos repositórios, as tags mais recentes e a formulação de revisão de método foram verificados em 2026-06-28.