Verification
The Lumenary aims to be more trustworthy than ordinary AI-generated material. This page reports exactly what has been checked, by what, and what has not.
Formal proofs (Lean)
88 declarations compiled with leanprover/lean4:v4.35.0; 0 depend on sorry. 3 apply a library theorem, 59 are proved here, 26 are definitions.
Generated 2026-10-28 06:13
Formal lab →Computational experiments (Python)
12 of 12 experiments ran and passed their tests. pytest: 571 passed, 0 failed.
Python 3.10.12 · sympy 1.13.3 · mpmath 1.3.0 · numpy 2.2.5 · pytest 8.3.5 · Generated 2026-10-28 06:13
Content validation
105 automated checks passed, 0 failed (schemas, prerequisite graph, registries, translations, answer parsing).
Browser end-to-end checks (six locales, exercises, graph, Python sandbox): 15 passed, 0 failed.
Generated 2026-10-28 06:16
Human review
No lesson, translation or exercise has yet been reviewed by a qualified human mathematician, educator or translator. Agreement among AI systems is not treated as evidence of correctness.
| Experiment | Evidence | Status |
|---|---|---|
| Cantor's diagonal trick on a finite list | Exact computation | passed |
| Clock arithmetic: which residues have inverses? | Exhaustive finite check, Exact computation | passed |
| Sorting and counting a market basket | Exact computation, Exhaustive finite check | passed |
| Composing functions: associative, but order matters | Exhaustive finite check, Counterexample | passed |
| Counting functions, injections and surjections | Exhaustive finite check, Exact computation | passed |
| Forty primes in a row, then a counterexample | Experimental evidence, Counterexample | passed |
| Exact versus numerical: 0.1 + 0.2 and the square root of 2 | Numerical approximation, Exact computation, Symbolic computation | passed |
| Hunting for inverses in the integers and the rationals | Experimental evidence, Exact computation | passed |
| Does a random walk come home? Statistical evidence | Statistical evidence, Exact computation | passed |
| Remainder families: residue classes that add up | Exhaustive finite check, Counterexample | passed |
| Checking set identities exhaustively | Exhaustive finite check, Counterexample | passed |
| Negative times negative: grid, symbols and proof | Experimental evidence, Symbolic computation | passed |
Known limitations
- Only five lessons and seven Wonder Trails exist; every other topic is planned.
- Lean proofs use core Lean 4 only; Mathlib integration is planned.
- The Pyodide (browser) runtime and the CPython test runtime are different Python versions; the experiments were checked to print identical output, but that check is not yet automated.
- No accessibility audit has been carried out.
- The language and country registries contain entries flagged for review.
Areas requiring human review
- Every lesson, trail, exercise and solution (mathematical accuracy)
- Age-appropriateness and pedagogy, especially of the K–2 and Grades 3–5 material
- Historical claims and attributions
- All machine-drafted translations and terminology glossaries
- Registry entries marked “needs review”
- Placement of topics and prerequisite edges in the curriculum map