01 / Límite
Mantener pequeña la base de confianza
No coloque generadores complejos ni IA en el centro de la confianza. Haga explícito el lado pequeño de comprobación.
Finite Field / Laboratorio matemático
Construir evidencia de corrección, no solo resultados rápidos.
El laboratorio matemático muestra cómo tratamos el modelado matemático, la demostración de teoremas, la verificación formal, la reproducibilidad y la implementación fiable sin exagerar la evidencia.
- Proyectos públicos
- NPA / STD / MATHLIB
- Lenguaje principal
- Rust
- Instantánea de NPA
- v0.1.1
Auditoría de pruebas / vista conceptual
Solo lectura
01 bytes canónicos / formato OK
02 hash del certificado OK
03 comprobación de pruebas dependientes OK
04 veredicto sin fuente OK
Límite de confianza visible
Esta página no afirma que NPA sea un sustituto práctico de Lean o Rocq, y la simulación del navegador no ejecuta NPA.
Principio del laboratorio
Publicar no solo resultados, sino también el límite de la comprobación.
Una conclusión como “funcionó”, “fue rápido” o “quedó demostrado” no basta. Mostramos por separado entradas, supuestos, partes confiables, artefactos comprobables de forma independiente y cuestiones no resueltas.
02 / Evidencia
Convertir la evidencia en artefacto
Deje certificados, hashes, listas de supuestos, condiciones de referencia y registros en una forma que otros puedan inspeccionar.
03 / Reproducir
Diseñar para la reproducibilidad
Fije cadenas de herramientas, datos de entrada, comandos de ejecución y criterios para que el resultado pueda comprobarse de nuevo.
04 / Honestidad
No exagerar el estado de la investigación
Muestre por separado métodos prácticos, experimentos e investigación. Coloque las limitaciones junto a los resultados.
REVISIÓN DE MÉTODO
Categoría de método de servicio que aún requiere alcance, responsabilidad, evidencia de cliente y aprobación antes de describirse como lista para proyecto.
EXPERIMENTAL
Existe una implementación funcional, pero aún pueden cambiar escala, compatibilidad, rendimiento o especificación. Se requieren versión y pasos de reproducción.
INVESTIGACIÓN
El diseño, la evaluación, la prueba o la implementación están en curso. Esto no implica disponibilidad comercial ni finalización.
Portafolio de investigación
Ver la investigación por madurez y artefactos.
Cada tarjeta muestra madurez, artefactos, estado actual y siguiente validación. La búsqueda y los filtros usan solo estado del navegador.
8 mostradas
EXPERIMENTAL
CÓDIGO ABIERTO
01
Nano Proof Auditor
Cadena de herramientas de prueba basada en certificados
Cadena de herramientas de investigación que coloca certificados de prueba canónicos y una base pequeña de comprobación en el centro de la revisión de pruebas dependientes.
- Artefactos
- fuente / especificación / plantillas de CI
- Actual
- instantánea pública v0.1.1
- Siguiente validación
- paquetes externos de teoremas y comprobación independiente
EXPERIMENTAL
CÓDIGO ABIERTO
02
NPA Standard Library
Logic / Nat / List / Algebra
Repositorio de paquetes de teoremas estándar para bases reutilizables de NPA.
- Artefactos
- fuente / paquetes de prueba
- Actual
- repositorio público separado
- Siguiente validación
- alcance del paquete y compatibilidad
INVESTIGACIÓN
CÓDIGO ABIERTO
03
NPA Math Library
Biblioteca matemática formal
Dirección de biblioteca para almacenar teoremas matemáticos como paquetes de prueba comprobables de forma independiente.
- Artefactos
- fuente / paquetes de prueba
- Actual
- repositorio público en desarrollo
- Siguiente validación
- estructura de biblioteca y auditoría de dependencias
REVISIÓN DE MÉTODO
MÉTODO
04
Modelos de planificación con restricciones
Programación / Rutas / Asignación
Método para separar restricciones duras y métricas de evaluación en turnos, visitas, rutas, producción y asignación.
- Artefactos
- modelo / prototipo / informe explicativo
- Actual
- método de servicio; la afirmación pública se limita a revisión de método
- Siguiente validación
- evidencia de cliente y aprobación de alcance
INVESTIGACIÓN
MEDICIÓN
05
Evaluación reproducible de solucionadores
Referencia de comparación y evidencia
Programa para fijar conjuntos de instancias, hardware, límites de tiempo, semillas aleatorias y registros brutos antes de hacer afirmaciones de rendimiento.
- Artefactos
- registro de referencias / registros brutos / informe
- Actual
- diseño de programa de investigación
- Siguiente validación
- primer corpus público de referencia
INVESTIGACIÓN
MÉTODOS FORMALES
06
Verificación para lógica empresarial crítica
Invariantes para sistemas empresariales
Investigación sobre cómo separar tarifas, permisos, inventario y transiciones de estado en especificaciones e invariantes.
- Artefactos
- especificación / invariantes / informe de prueba o demostración
- Actual
- estudio de alcance
- Siguiente validación
- seleccionar un caso acotado similar a producción
EXPERIMENTAL
INGENIERÍA
07
Componentes pequeños de confianza en Rust
Componentes pequeños de confianza
Trabajo de implementación que mantiene piezas críticas de confianza, como verificadores y hashes, suficientemente pequeñas para inspección.
- Artefactos
- núcleo NPA / crate de certificado / verificador de referencia
- Actual
- implementación pública en NPA
- Siguiente validación
- compatibilidad del verificador independiente
INVESTIGACIÓN
IA × PRUEBA
08
Asistencia de IA y comprobación independiente
Generar libremente, verificar estrictamente
Dirección de investigación que sitúa la IA en la generación de candidatos mientras la evidencia final se comprueba de forma independiente.
- Artefactos
- generador de candidatos / certificado / informe del verificador
- Actual
- dirección de investigación coherente con el modelo de confianza de NPA
- Siguiente validación
- flujo de autoría medido
No se encontró ningún área de investigación coincidente.
Pruebe otra palabra clave o devuelva el filtro de madurez a Todos.
Nano Proof Auditor
Separar la generación de pruebas de aquello en lo que confiamos.
NPA es una cadena de herramientas de prueba basada en certificados para pruebas dependientes. Interfaces, tácticas, búsqueda de teoremas, complementos, IA, archivos fuente y estado de CI pueden ayudar a crear candidatos, pero no son la evidencia de prueba fiable.
EXPERIMENTALCÓDIGO ABIERTOAPACHE-2.0
Instantánea actual
v0.1.1
Información pública comprobada el 2026-06-21.
Núcleo principal
Rust
El verificador y el núcleo Rust forman parte del lado de comprobación.
Artefacto de auditoría
.npcert
Los bytes canónicos del certificado son el objeto que se inspecciona.
Punto de recomprobación
revisión manual
El estado del repositorio y la visibilidad del paquete deben revisarse antes de publicar.
Explorador del límite de confianza
Explore qué se considera confiable y qué no.
Pulse cada nodo para inspeccionar qué hace, qué produce y qué comprobación sigue siendo necesaria.
NO CONFIABLE
COMPROBADO
Límite importante
NPA no es actualmente un sustituto práctico de Lean o Rocq. Esta página explica un diseño de investigación centrado en certificados y no garantiza sistemas comerciales sin errores ni resolución automática de teoremas.
Comprobación de certificados / simulación explicativa
Experimente el flujo de comprobación de certificados.
La interacción del navegador explica el flujo de inspección. No ejecuta NPA, Rust, WASM ni certificados de prueba reales.
Ejemplo de CLI
npa package verify-certs --root . --checker reference --json
NPA / traza de auditoría
LISTO
- 01 Leer el certificadobytes canónicos / formato ESPERAR
- 02 Comprobar el hash del certificadohash del certificado ESPERAR
- 03 Comprobar con el núcleocomprobación de pruebas dependientes ESPERAR
- 04 Recomprobar con el verificador de referenciaveredicto sin fuente ESPERAR
- 05 Comparar el informe de axiomashash del informe de axiomas ESPERAR
Veredicto
La explicación aún no se ha ejecutado.Ejecute la explicación para visualizar los pasos en orden.
Ecosistema de pruebas
Aclarar roles en lugar de clasificar herramientas.
Lean y Rocq son ecosistemas maduros de asistentes de prueba. NPA se muestra aquí como un proyecto de investigación e implementación centrado en certificados, no como una clasificación de sustitutos.
| 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 basada 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 y comprobación independiente. |
| Énfasis | Extensibilidad, bibliotecas y pruebas interactivas. | Expresividad, métodos maduros y bibliotecas. | Base de confianza pequeña y certificados canónicos. |
| 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. |
| Límite | Sigue siendo necesario conocimiento especializado. | Sigue siendo necesario conocimiento especializado. | No pretende ser un sustituto práctico de Lean o Rocq en este momento. |
Método de investigación
Convertir “funcionó” en un procedimiento de comprobación repetible.
Un resultado se fortalece cuando alguien puede repetirlo, inspeccionarlo y rechazarlo bajo las mismas condiciones.
Pregunta
Definir qué debe comprobarse: rendimiento, corrección, compatibilidad o alcance.
Supuestos
Escribir supuestos, exclusiones, axiomas, brechas de datos y sesgos antes de evaluar.
Artefacto
Conservar fuente, certificados, entradas, registros de ejecución y hashes.
Comprobación independiente
Comprobar los resultados por una ruta diferente al lado de generación.
Referencia de comparación
Fijar hardware, versiones, límites de tiempo, conjuntos de instancias y semillas aleatorias.
Límites
Publicar fallos, casos no soportados, límites de rendimiento y siguiente validación.
Constructor de reproducibilidad
Compruebe qué falta aún en una publicación de investigación.
La lista de comprobación se procesa solo en el navegador. No es una puntuación de certificación.
Preparación
0%Siguiente acción
Defina primero la pregunta de investigación y la condición de éxito.Antes de decidir formatos de artefacto, fije qué se comparará o comprobará.
Artefactos públicos
Rastrear artefactos públicos desde una entrada.
La página evita llamadas a la API de GitHub en tiempo de ejecución. El estado del repositorio es una instantánea revisada que debe comprobarse antes de publicar.
4 artefactos
finitefield-org
npa
cadena de herramientas de prueba basada en certificados
VERIFICAR
package verify-certs
finitefield-org
npa-std
paquete estándar de teoremas
ROL
Std.Logic / Nat / List
finitefield-org
npa-mathlib
biblioteca matemática formal
ROL
paquetes de teoremas formales
GitHub
finitefield-org
índice de repositorios públicos
ÍNDICE
todos los repositorios públicos
Ningún artefacto público coincide con la búsqueda.
Política de publicación
Repositorios públicos, notas de investigación y referencias de comparación deben incluir fecha comprobada, madurez, pasos de reproducción y limitaciones conocidas. Las estrellas y los recuentos de commits no se muestran como señales de calidad de investigación.
Del laboratorio a las operaciones
Llevar disciplina de investigación al diseño de sistemas empresariales.
No todos los sistemas de cliente necesitan demostración de teoremas. La transferencia útil consiste en decidir qué debe confiarse, compararse, comprobarse, corregirse y aprobarse por personas.
Práctica de laboratorio
Separe generación, cálculo y comprobación final en lugar de confiar por igual en todas las capas.
Conserve entradas, salidas, certificados, hashes y registros como artefactos revisables.
Fije datos, versiones, comandos y criterios de evaluación antes de comparar resultados.
Publique restricciones, casos fallidos y puntos no resueltos con el mismo peso que los resultados.
Sistema del cliente
Defina quién introduce datos, quién revisa, quién anula y quién confirma el resultado.
Muestre restricciones, puntuaciones de evaluación, candidatos rechazados y puntos no resueltos.
Conserve cambios de condiciones, ejecuciones de cálculo e historial de aprobación final.
Haga que la salida automatizada pueda corregirse, rechazarse y explicarse a los operadores.
01
Turnos y dotación
Muestre por separado las infracciones de reglas y el cumplimiento de preferencias.
02 Rutas de vehículosMantenga visibles los motivos de ruta, la capacidad, las ventanas horarias y las excepciones.
03 Programación de producciónExplique el trabajo sin programar, los cuellos de botella y las compensaciones de preparación.
04 Asignación y emparejamientoMuestre motivos de candidatos y alternativas antes de la aprobación.
Notas de investigación
Mantener legibles el historial de actualización y la evidencia.
No todas las tarjetas son artículos publicados. Las notas en preparación no se etiquetan como trabajo publicado hasta tener fechas, fuentes y pasos de reproducción.
NPA / actual
Por qué poner los certificados en el centro
Por qué la evidencia final debe ser un certificado estandarizado comprobado por una ruta pequeña e independiente.
Ver repositorio públicoNota de diseño / planificada
Hacer explicables los resultados de optimización
Nota de diseño sobre cómo exponer objetivos, restricciones duras, preferencias blandas y asignaciones no resueltas en la interfaz.
Ver demostraciones relacionadasReferencia de comparación / planificada
Condiciones para comparar solucionadores de forma justa
Nota planificada sobre conjuntos de instancias, límites de tiempo, brechas de optimalidad, semillas aleatorias y hardware.
Ver criterios de publicaciónLos elementos “En preparación” no son artículos publicados. Después de publicarse, cada nota recibe fecha, fuente, autor, ruta de reproducción y limitaciones conocidas.
PREGUNTAS FRECUENTES
Límites de investigación, herramientas de prueba y uso empresarial.
Estos puntos se explicitan para que las páginas de investigación no se confundan con garantías de producción.
Leer sobre la empresa01 ¿El laboratorio matemático es un servicio de desarrollo contratado?
No. Es un lugar para publicar actitud de investigación y artefactos. En conversaciones con clientes, separamos métodos aplicables, métodos que necesitan más validación y temas en fase de investigación.
02 ¿Puede NPA sustituir a Lean o Rocq?
No. El NPA actual no es un sustituto práctico de Lean o Rocq. Es un proyecto de investigación e implementación sobre certificados, comprobación independiente y una base de confianza pequeña.
03 ¿Confían tal cual en las pruebas generadas por IA?
No. La IA, la búsqueda y las tácticas ayudan a generar candidatos. Nos centramos en si el certificado final es aceptado por un verificador independiente de esas rutas de generación.
04 ¿La verificación formal elimina todos los errores?
No. Los métodos formales comprueban propiedades concretas frente a una especificación explícita. Especificaciones incorrectas, código fuera de alcance, operaciones y servicios externos aún necesitan revisión separada.
05 ¿Esto se relaciona con el trabajo en sistemas empresariales?
Sí. Normalmente aplicamos la disciplina de forma gradual: restricciones, motivos del resultado, historial de cálculo, límites de permisos y comprobaciones de lógica empresarial importante.
Consultar un problema
Puede consultar el trabajo que quiere resolver, no solo el tema de investigación.
Empezando por la hoja de cálculo actual, las reglas y los puntos donde las personas corrigen decisiones, podemos ordenar si debe ir primero el modelado matemático, la automatización de reglas o un prototipo.
Instantánea de fuentes / 2026-06-21
Las afirmaciones sobre NPA se basan en la instantánea del repositorio finitefield-org/npa. La posición de Lean y Rocq se basa en sus sitios oficiales. El estado del repositorio, las etiquetas más recientes y la formulación de revisión de método se comprobaron el 2026-06-28.