Estado público
Repositorio de investigación e implementación
El repositorio de GitHub es público, pero esta página describe un repositorio de investigación e implementación, no un servicio desplegado.
Volver al laboratorio matemático
NPA / Comprobación de pruebas centrada en certificados
NPA: mostrar el límite de la evidencia antes de confiar en un resultado.
Esta página reconstruye la sección NPA del laboratorio matemático como una página de evidencia independiente: estado público, modelo de confianza, proceso de prueba, registro de afirmaciones, repositorios, fuentes y lenguaje explícito de no sustitución.
- Estado público
- Repositorio de investigación
- Se muestra como investigación e implementación, no como servicio de garantía en producción.
- Comprobación pública
- 2026-07-02 / NPA v0.2.0
- Últimas etiquetas Git comprobadas: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- Licencia
- Apache-2.0
- Apache-2.0 se verificó para npa, npa-std y npa-mathlib el 2026-07-02.
Comprobación pública: 2026-07-02. La última etiqueta Git del repositorio NPA es v0.2.0; npa-std es v0.1.0; npa-mathlib es v0.1.30. Las versiones fijadas en los archivos README se muestran como contexto específico de cada repositorio y no se agrupan en una sola afirmación de versión de NPA.
Estado público
Indicar qué es público, qué constituye evidencia y cuándo se volvió a comprobar.
Esta página hace visible su base: una instantánea local de datos, una fuente pública de repositorio y la fecha de la revisión final previa al lanzamiento.
Comprobación pública
2026-07-02
La revisión de fuentes públicas terminó el 2026-07-02. La reconstrucción original sigue usando la instantánea local de datos del 2026-06-21.
Evidencia
Certificados y hashes
La instantánea de fuentes registra .npcert canónico, certificate_hash, export_hash, axiom_report_hash y veredictos de los comprobadores.
Licencia
Apache-2.0 verificada
Apache-2.0 se verificó para npa, npa-std y npa-mathlib mediante metadatos públicos del archivo LICENSE el 2026-07-02.
Límite
NPA no es un sustituto práctico de Lean ni de Rocq. La simulación distribuida de inspección del navegador no ejecuta NPA. Las etiquetas públicas, la licencia y la visibilidad de los repositorios se comprobaron el 2026-07-02 para la revisión final antes de publicar.
Límite de confianza
Cruzar el límite de evidencia solo con un certificado canónico.
El límite no depende de qué herramienta parezca sofisticada, sino de qué artefacto puede convertirse en evidencia tras una comprobación independiente.
El analizador, elaborador, tácticas, automatización, búsqueda de teoremas, complementos, sistemas de IA, archivos fuente, archivos de repetición, índices de teoremas, planes de publicación, estado de CI, páginas de versiones y metadatos de registro permanecen en el lado no fiable de los candidatos.
Proceso de prueba / simulación explicativa
Mostrar el proceso exacto desde los bytes del certificado hasta la evidencia de comprobación.
La simulación del navegador no ejecuta NPA, Rust, WASM ni certificados de prueba reales. Visualiza el orden de comprobación sin código fuente que deben satisfacer los artefactos reales.
Ruta de evidencia de CLI
npa package verify-certs --root . --checker reference --json
NPA / traza de auditoría
LISTO
- 01 Formato del certificadobytes canónicos .npcert / certificado analizable / comprobación de formato ESPERAR
- 02 Hash del certificadobytes del certificado / certificate_hash / resumen determinista ESPERAR
- 03 Veredicto del núcleocertificado / aceptar o rechazar / informe del verificador Rust ESPERAR
- 04 Comprobador de referenciacertificado fijado por hash / aceptación o rechazo independiente / informe del comprobador sin fuente ESPERAR
- 05 Informe de axiomaspaquete comprobado / axiom_report_hash / inventario de supuestos ESPERAR
Veredicto
El proceso explicativo aún no se ha ejecutado.Ejecute la explicación para marcar en orden la ruta de comprobación sin código fuente.
Registro de afirmaciones
Separar la evidencia, los hechos sujetos al tiempo y las afirmaciones de límite.
La página no depende de textos de investigación imprecisos. Cada declaración pública está vinculada a una instantánea local de referencia, una fuente y una acción de publicación.
| Afirmación | Redacción pública | Estado | Fuente | Acción de publicación |
|---|---|---|---|---|
| CL-001 | NPA prioriza el certificado: el límite auditable es el artefacto canónico .npcert y la ruta de comprobación que lo rodea. | Afirmación pública verificada | S01 / 2026-07-02 | Revisar cuando cambie el archivo README. |
| CL-002 | La revisión pública del 2 de julio de 2026 constató que la etiqueta Git más reciente del repositorio de NPA era v0.2.0. Los archivos README de los paquetes relacionados siguen mostrando referencias específicas de cada repositorio, por lo que la redacción de las versiones se mantiene limitada a cada repositorio. | Revisión pública verificada | S01 / S02 / 2026-07-02 | Mantener la redacción de etiquetas limitada a cada repositorio. |
| CL-003 | La instantánea local de referencia registra una versión fijada de la cadena de herramientas Rust 1.95.0; no se utiliza como afirmación comercial. | Verificado, sujeto al tiempo | S01 / 2026-07-02 | Volver a comprobar si se muestra la versión de la cadena de herramientas. |
| CL-004 | NPA no es un sustituto práctico de Lean ni de Rocq. Este límite debe permanecer visible junto a cualquier comparación. | Afirmación de límite verificada | S01 / S03 / S05 / 2026-07-02 | Conservar la advertencia. |
| CL-005 | npa-std y npa-mathlib son repositorios públicos independientes de paquetes de teoremas dentro de la organización finitefield-org. | Afirmación pública verificada | S01 / S02 / 2026-07-02 | Volver a comprobar la visibilidad de los repositorios si la publicación se retrasa o si cambian los repositorios. |
| CL-006 | Los repositorios npa, npa-std y npa-mathlib muestran cada uno la licencia Apache-2.0 mediante sus metadatos públicos del archivo LICENSE. | Afirmación pública verificada | S01 / S02 / 2026-07-02 | Volver a comprobar el archivo LICENSE en una versión principal. |
Repositorios y licencia
Hacer explícitos el código, los repositorios de paquetes y la visibilidad de la organización.
Los enlaces a repositorios remiten a fuentes públicas; no garantizan que esta página esté sincronizada con el último estado de GitHub.
4 repositorios mostrados
finitefield-org
npa
Herramientas de asistencia y verificación de pruebas centradas en certificados.
- Licencia
- Apache-2.0 verificada mediante el archivo LICENSE el 2026-07-02.
- Verificación
- Última etiqueta Git: v0.2.0. No se ha publicado una versión más reciente en GitHub. Referencia actual de herramientas en README: NPA_GIT_TAG=v0.2.0.
experimentalRust / OCamlcentrado en certificados
Abrir repositorio
finitefield-org
npa-std
Repositorio del paquete estándar de teoremas para fuentes de prueba de NPA.
- Licencia
- Apache-2.0 verificada mediante el archivo LICENSE el 2026-07-02.
- Verificación
- Última etiqueta Git y versión de GitHub: v0.1.0. Versión de metadatos del paquete en README: 0.1.0; versión fijada de herramientas del paquete: NPA_GIT_TAG=v0.1.1.
experimentalpaquete de teoremasfuente de prueba
Abrir repositorio
finitefield-org
npa-mathlib
Repositorio de investigación de una biblioteca de matemáticas formales.
- Licencia
- Apache-2.0 verificada mediante el archivo LICENSE el 2026-07-02.
- Verificación
- Última etiqueta Git: v0.1.30. Última versión de GitHub: v0.1.9. Versión de metadatos del paquete en README: 0.2.1; versión fijada de herramientas del paquete: NPA_GIT_TAG=v0.1.1.
investigaciónmatemáticas formalesbiblioteca
Abrir repositorio
finitefield-org
Organización GitHub de Finite Field
Instantánea pública de la organización para la familia de repositorios del laboratorio.
- Licencia
- Se aplican licencias específicas de cada repositorio
- Verificación
- npa, npa-std y npa-mathlib son públicos según la comprobación de la API de GitHub del 2026-07-02.
índice públicoinstantánea de visibilidadfuente
Abrir organización
Ningún repositorio coincide con la búsqueda actual.
Los repositorios de GitHub son la fuente del estado público del código. La licencia, las etiquetas actuales, la visibilidad pública y el texto de las versiones se comprobaron el 2026-07-02 en la revisión final M10-T14.
Salvaguarda del ecosistema de pruebas
Aclarar las funciones antes de comparar herramientas de prueba.
Esta es una tabla de funciones, no una clasificación. Lean y Rocq siguen siendo los ecosistemas de referencia para asistentes de pruebas; NPA se presenta como trabajo de investigación e implementación centrado en certificados.
| Elemento | Lean | Rocq | NPA |
|---|---|---|---|
| Posición | Lenguaje de programación y asistente de pruebas de código abierto. | Demostrador interactivo de teoremas con una larga trayectoria de investigación. | Repositorio de investigación e implementación para comprobación centrada en certificados. |
| Uso habitual | Matemáticas, verificación de software y programación. | Matemáticas, especificaciones, verificación de programas y extracción. | Investigación sobre certificados de prueba, comprobación independiente y una base de confianza reducida. |
| Límite de la evidencia | Su propio núcleo de confianza y su ecosistema definen el límite de comprobación. | Su propio núcleo y los desarrollos comprobados definen el límite de comprobación. | El artefacto canónico .npcert pasa de la generación a la comprobación. |
| Cómo lo trata esta página | Referencia para aprendizaje, comparación e interoperabilidad. | Referencia para aprendizaje, comparación y métodos de formalización. | Proyecto de investigación de Finite Field, no una promesa de producto. |
| Límite | Siguen siendo necesarios conocimientos especializados. | Siguen siendo necesarios conocimientos especializados. | Actualmente, NPA no es un sustituto práctico de Lean ni de Rocq. |
Fuentes
Publicar el mapa de fuentes junto a la interpretación.
Las fuentes permiten distinguir qué afirmaciones proceden de repositorios públicos, sitios oficiales de herramientas de prueba y contexto empresarial.
S01
finitefield-org/npa
Fuente principal sobre el propósito y el modelo de confianza de NPA, el texto de la etiqueta actual v0.2.0, los comandos, la estructura del repositorio y la licencia.
Abrir fuente S02Organización GitHub de Finite Field
Fuente principal sobre visibilidad pública de repositorios, últimas etiquetas Git, páginas de versiones y la instantánea de la familia de repositorios del laboratorio comprobada el 2026-07-02.
Abrir fuente S03Sitio oficial de Lean
Fuente principal sobre la posición pública de Lean, comprobada el 2026-07-02.
Abrir fuente S04Referencia del lenguaje Lean
Fuente principal sobre teoría de tipos dependientes y contexto de referencia del núcleo, comprobada el 2026-07-02.
Abrir fuente S05Sitio oficial de Rocq Prover
Fuente principal sobre la posición pública de Rocq, comprobada el 2026-07-02.
Abrir fuente S06Sitio corporativo de Finite Field
Fuente corporativa sobre la marca Finite Field y el contexto empresarial.
Abrir fuentePREGUNTAS FRECUENTES
Estado de NPA y límites de verificación.
Las respuestas destacan el límite de confianza antes de que el lector confunda una página de investigación con un servicio de asistencia de pruebas desplegado.
Conocer la empresa01 ¿Esta página es una garantía de producto?
No. NPA se presenta aquí como repositorio de investigación e implementación.
02 ¿Puede NPA sustituir a Lean o Rocq?
No. NPA no es un sustituto práctico de Lean ni de Rocq.
03 ¿La página ejecuta una verificación real de NPA?
No. La simulación del navegador no ejecuta NPA, Rust, WASM ni certificados de prueba reales.
04 ¿Qué se considera evidencia aquí?
El artefacto de certificado, los hashes deterministas, el resultado del núcleo/verificador Rust, el resultado del comprobador de referencia sin código fuente y el informe de axiomas forman la evidencia del lado de comprobación.
05 ¿Qué datos deben volver a comprobarse?
La versión pública actual, la visibilidad de los repositorios, las versiones fijadas de las herramientas, el texto de la licencia y la redacción de las fuentes se volvieron a comprobar el 2026-07-02.
De la disciplina de prueba a las operaciones
Aplicar la misma disciplina de evidencia cuando una decisión empresarial debe ser fiable.
Para los sistemas empresariales, la lección útil no es añadir demostración de teoremas en todas partes. Es decidir qué deben generar, comprobar, registrar, corregir y aprobar las personas.