Verificación
The Lumenary aspira a ser más fiable que el material corriente generado por IA. Esta página informa exactamente de lo que se ha comprobado, con qué, y de lo que no.
Demostraciones formales (Lean)
88 declaraciones compiladas con leanprover/lean4:v4.35.0; 0 dependen de sorry. 3 aplican un teorema de biblioteca, 59 se demuestran aquí y 26 son definiciones.
Generado el 2026-10-28 06:13
Laboratorio formal →Experimentos computacionales (Python)
12 de 12 experimentos se ejecutaron y superaron sus pruebas. pytest: 571 superadas, 0 fallidas.
Python 3.10.12 · sympy 1.13.3 · mpmath 1.3.0 · numpy 2.2.5 · pytest 8.3.5 · Generado el 2026-10-28 06:13
Validación del contenido
105 comprobaciones automáticas superadas, 0 fallidas (esquemas, grafo de requisitos previos, registros, traducciones, análisis de respuestas).
Comprobaciones de extremo a extremo en el navegador (seis idiomas, ejercicios, grafo, entorno de Python): 15 superadas, 0 fallidas.
Generado el 2026-10-28 06:16
Revisión humana
| Experimento | Evidencia | Estado |
|---|---|---|
| Cantor's diagonal trick on a finite list | Cálculo exacto | superado |
| Clock arithmetic: which residues have inverses? | Comprobación finita exhaustiva, Cálculo exacto | superado |
| Sorting and counting a market basket | Cálculo exacto, Comprobación finita exhaustiva | superado |
| Composing functions: associative, but order matters | Comprobación finita exhaustiva, Contraejemplo | superado |
| Counting functions, injections and surjections | Comprobación finita exhaustiva, Cálculo exacto | superado |
| Forty primes in a row, then a counterexample | Evidencia experimental, Contraejemplo | superado |
| Exact versus numerical: 0.1 + 0.2 and the square root of 2 | Aproximación numérica, Cálculo exacto, Cálculo simbólico | superado |
| Hunting for inverses in the integers and the rationals | Evidencia experimental, Cálculo exacto | superado |
| Does a random walk come home? Statistical evidence | Evidencia estadística, Cálculo exacto | superado |
| Remainder families: residue classes that add up | Comprobación finita exhaustiva, Contraejemplo | superado |
| Checking set identities exhaustively | Comprobación finita exhaustiva, Contraejemplo | superado |
| Negative times negative: grid, symbols and proof | Evidencia experimental, Cálculo simbólico | superado |
Limitaciones conocidas
- Solo existen cinco lecciones y siete Senderos del Asombro; todos los demás temas están planificados.
- Las demostraciones en Lean usan solo el núcleo de Lean 4; la integración con Mathlib está prevista.
- El entorno de ejecución de Pyodide (navegador) y el de pruebas de CPython usan versiones distintas de Python; se comprobó que los experimentos imprimen la misma salida, pero esa comprobación aún no está automatizada.
- No se ha realizado ninguna auditoría de accesibilidad.
- Los registros de idiomas y de países contienen entradas marcadas para revisión.
Áreas que requieren revisión humana
- Cada lección, sendero, ejercicio y solución (exactitud matemática)
- Adecuación a la edad y pedagogía, especialmente del material de preescolar a 2.º y de 3.º a 5.º grado
- Afirmaciones y atribuciones históricas
- Todas las traducciones redactadas automáticamente y los glosarios de terminología
- Entradas del registro marcadas como «requiere revisión»
- Ubicación de los temas y de las aristas de requisitos previos en el mapa del plan de estudios