ReasBook
ReasBook es un proyecto Lean 4 para formalizar matemáticas a partir de libros y artículos científicos, preservando la estructura original mientras produce enunciados y demostraciones verificables por máquina.
Ficha actualizada 23 sept 2026, 16:10 · upstream 23 sept 2026, 15:45 · release reasbook-site-20260922T120928Z-7eedc92b59ac
Qué es ReasBook
Descripción editorial construida a partir del repositorio, su documentación y sus señales de mantenimiento.
ReasBook separa las fuentes matemáticas versionadas de los herramientas de verificación cruzada. El repositorio contiene el catálogo oficial del proyecto, que incluye libros y artículos formales con enlaces directos a sus ramas correspondientes en Lean. Se puede descargar un libro individual mediante Git sparse-checkout sin descargar todo el repositorio. Para desarrollo local, generación de documentación y despliegue estático se recomienda utilizar la SDK enfocada en cada capacidad específica.
El proyecto cuenta con una plataforma de revisión integrada (ReasBook Reviewer) que permite a los usuarios leer los libros formales y enviar comentarios firmados. La plataforma soporta almacenamiento persistente de comentarios y autenticación mediante ReasLab, además de integración con GitHub Pages para publicaciones estáticas.
- Formalizar matemáticas desde libros y artículos científicos (ej. Álgebra Topológica, Análisis II, Teoría de Grupos Combinatoriales)
- Visualización de dependencias entre teoremas mediante mapas interconectados
- Plataforma de lectura y revisión colaborativa de libros formales
- Comparación automática de soluciones en problemas matemáticos
- Generación de documentación técnica para desarrolladores
- Soporta múltiples ramas de Lean (v4.26, v4.30, v4.32) con sincronización cruzada
- Integración con M2F para generar proyectos formales desde referencias existentes
- Quokka: sistema automatizado para convertir literatura matemática en proyectos Lean compilables
- Separación clara entre fuentes versionadas y herramientas de verificación
- Plataforma de revisión colaborativa con comentarios firmados
- El catálogo del proyecto está vacío (no incluye libros formales activos)
- Requerimiento de Git 2.25 o superior para usar sparse-checkout
- No hay comentarios públicos sin backend de revisión implementado
- La documentación Verso no ha sido publicada oficialmente
- Dependencia de ReasLab para autenticación y almacenamiento persistente
Perfil de infraestructura
Estimación inicial derivada del repositorio y de los servicios detectados.
Despliegue detectado
Qué señales reales de instalación hemos encontrado.
Para desplegar ReasBook, se recomienda usar Docker Compose con la configuración del repositorio. Se pueden crear contenedores separados para el servidor de lectura (port 8876), el catálogo web (port 3000) y la plataforma de revisión. Para producción, se debe configurar un backend de autenticación seguro (OAuth2 o JWT) en ReasLab, almacenar comentarios permanentemente y desplegar GitHub Pages como destino público. Se recomienda mantener los repositorios de Lean en ramas aisladas para cada versión y usar el SDK como punto de acceso centralizado.
Stack y dependencias
Componentes inferidos a partir de manifests, configuración y documentación.
Experiencia real de la comunidad
Ayuda a contrastar la estimación automática con instalaciones reales.
Todavía no hay datos comunitarios para este proyecto.