The Lumenary — evaluation package for educators

1. Mission and philosophy

The Lumenary is a free, open-source mathematics curriculum, designed to run from kindergarten to the first year of graduate school, with optional research pathways. It is inspired by historic Christian values — truthfulness, humility, generosity, love of neighbour — but requires no belief of any learner, and justifies every mathematical statement mathematically.

Its pedagogical commitments are: understanding over memorisation; productive struggle with progressive hints; no shame-based feedback, compulsory streaks or rankings; respect for different learning speeds; accessibility; and no paid subscriptions. The guiding principle is Master the present. Glimpse the future. Never require the future to understand the present.

2. Three integrated modes of reasoning

Every lesson interleaves Human reasoning (intuition, examples, conventional proofs), Formal reasoning (Lean 4 definitions and machine-checked proofs) and Computational reasoning (Python experiments with explicit labels for the kind of evidence produced). A "lens" control lets a reader highlight one mode at a time. For young children the formal mode becomes age-appropriate logic games; Lean code appears only in collapsible "for grown-ups" panels.

3. Curriculum map

Nivel	temas en el mapa	Lección disponible
Preescolar a 2.º	9	Collections, Counting, Addition, subtraction and place value to 100, Patterns, Shapes, Measuring length and time, Data, tallies and picture graphs, Doing and undoing, Following and giving precise instructions
3.º a 5.º grado	15	Sets, True, false, and, or, not, Whole-number arithmetic, Fractions and decimals, Factors, multiples and primes, Expressions, unknowns and rules, Area, perimeter and angles, Symmetry: slides, turns and flips, Estimation and rounding, Systematic listing and counting, Dots and lines: networks and puzzles, Data displays and the mean as a fair share, One thing after another, Repetition and decisions, Secret codes
6.º a 8.º grado	21	Functions, Relations, equivalence relations and partitions, Set-builder notation, quantifiers and infinite sets, Integers, Clock arithmetic: remainders and modular arithmetic, Rational numbers, Ratios, rates and proportional reasoning, Variables and algebraic expressions, Linear equations and inequalities, Linear relationships and simultaneous equations, The coordinate plane, The Pythagorean theorem, Rigid motions, congruence and similarity, Graphs of change, Counting principles, Statistics: centre, spread and distributions, Probability, Function machines in sequence, Diagrams where paths agree, Programming for mathematics, Check digits and error detection
9.º a 12.º grado	27	Propositional logic and truth tables, Proof: direct, contrapositive, contradiction and induction, Countability and Cantor's diagonal argument, Russell's paradox and why sets need axioms, Real numbers and irrationality, Complex numbers, Divisibility, Euclid's algorithm and unique factorisation, Polynomials, Quadratic equations and functions, Euclidean geometry and proof, Trigonometry, Functions and their graphs (precalculus), Exponential and logarithmic functions, Sequences and series, Introductory calculus, Combinatorics, Graphs, Conditional probability and independence, Sampling and statistical reasoning, Composition, Structure-preserving maps: homomorphisms and isomorphisms, Products by maps: a first universal property, Algorithms, correctness and efficiency, First steps in Lean, Mathematical modelling with functions, Vectors and coordinate geometry, Conic sections
Primeros años de universidad	23	Orders, lattices and well-orders, First-order logic, Congruences, Constructing ℤ, ℚ and ℝ, Linear algebra, Algebraic structures: monoids, groups and rings, Transformation geometry and the Erlangen programme, Calculus of one variable, Multivariable and vector calculus, Ordinary differential equations, Recurrences and generating functions, Probability theory, Statistical inference, Categories, Functors, Universal properties, Numerical methods, Algorithm design and analysis, Formalising mathematics in Lean and Mathlib, Classical mechanics, Cryptography, Surfaces, polyhedra and the Euler characteristic, Non-Euclidean geometry: spherical and hyperbolic
Universidad avanzada	39	ZFC: axiomatic set theory, Ordinals and cardinals, The axiom of choice and its equivalents, Completeness, compactness and Löwenheim–Skolem, Type theory and propositions as types, Mathematical writing, Number theory, Groups, Rings, ideals and fields, Quotient groups and quotient rings, Fields and Galois theory, Advanced linear algebra, Metric spaces and point-set topology, Differential geometry of curves and surfaces, Homotopy and the fundamental group, Real analysis, Complex analysis, Partial differential equations and Fourier series, Graph theory, Enumerative combinatorics, Markov chains, Natural transformations, Products, coproducts, initial and terminal objects, Limits and colimits, Adjunctions, Representable functors, The Yoneda lemma, Computability, The λ-calculus, Computational complexity, Numerical analysis, Optimisation, Information theory, Mathematical biology, Projective geometry, Differential forms and Stokes' theorem, Knot theory, Matrix groups and continuous symmetry, Dynamical systems and chaos
Primer año de posgrado	44	Model theory, Gödel's incompleteness theorems, Proof theory, Axiomatic set theory: hierarchy, cardinal arithmetic and L, Forcing and independence, Descriptive set theory, Reading the mathematical literature, Algebraic number theory, Modules, Commutative algebra, Representation theory of finite groups, Homological algebra, Quivers and path algebras, Algebraic topology, Smooth manifolds, Algebraic geometry, Sheaves, Measure theory and integration, Functional analysis, The probabilistic method, Measure-theoretic probability, Stochastic processes, Monads, Monoidal categories, Abelian categories, Enriched categories, Categorical logic, Elementary topos theory, Kan extensions, Formal methods, Computational reproducibility, Experimental mathematics: conjectures and counterexamples, Mathematical foundations of quantum mechanics, Riemannian geometry, Lie groups and Lie algebras, Differential topology, Homotopy theory, Vector bundles and characteristic classes, Riemann surfaces, Fourier and harmonic analysis, Partial differential equations: modern theory, Ergodic theory, Analytic number theory, The geometry of spacetime: special and general relativity
Caminos de investigación	22	Large cardinals, Homotopy type theory, Research ethics and attribution, Quiver representations, Higher categories, ∞-categories, Derived categories, Triangulated categories, Stable ∞-categories, Categorical representation theory, Formalising published mathematics, Low-dimensional topology: 3- and 4-manifolds, Geometric group theory, Symplectic geometry and topology, Complex and Kähler geometry; Hodge theory, Stable homotopy theory and generalised cohomology, Geometric analysis, Arithmetic geometry and elliptic curves, The Langlands programme: an orientation, Random structures: walks, percolation and random geometry, Gauge theory and the geometry of physics, Extremal and additive combinatorics

The complete map is browsable in the curriculum browser and the interactive knowledge graph. Required prerequisite edges form a directed acyclic graph (checked automatically); optional discovery edges link to Wonder Trails and never affect progression.

4. Foundations, structure and many viewpoints

Earlier mathematics emphasises sets; category theory is introduced gradually as a structural language for higher mathematics. Neither replaces the other — and neither is the only way of seeing. Geometry and topology run as a third thread from shapes and symmetry in the early grades to manifolds, homotopy theory and low-dimensional topology, and from early undergraduate level every lesson has a Viewpoints section showing its subject through the eyes of a topologist, geometer, analyst, algebraist, number theorist, probabilist, logician or physicist, as well as through sets and categories. Specialisation pathways cover geometry and topology, analysis and dynamics, algebra and number theory, and mathematical physics. The topics in each progression are:

5. Representative lessons

6. Wonder Trail demonstrations

• Boxes inside boxes

  → Sets, Russell's paradox and why sets need axioms, ZFC: axiomatic set theory

• Corners, edges and faces

  → Surfaces, polyhedra and the Euler characteristic, Algebraic topology, Riemannian geometry

• How many infinities?

  → Countability and Cantor's diagonal argument

• Primes forever

  → Divisibility, Euclid's algorithm and unique factorisation, Number theory, Analytic number theory

• Halfway to the wall

  → Sequences and series, Real analysis, Measure theory and integration

• Symmetry makes groups

  → Groups, Matrix groups and continuous symmetry, Lie groups and Lie algebras

• Knots and colours

  → Knot theory, Low-dimensional topology: 3- and 4-manifolds, Categorical representation theory

• Can a computer decide?

  → Computability, Gödel's incompleteness theorems, Computational complexity

• Clock arithmetic

  → Clock arithmetic: remainders and modular arithmetic, Congruences, Quotient groups and quotient rings

• Inverses and structure

  → Algebraic structures: monoids, groups and rings, Groups, Rings, ideals and fields

• Remainder families

  → Relations, equivalence relations and partitions, Congruences, Quotient groups and quotient rings

• The product, by its maps

  → Universal properties, Limits and colimits

• Life on a torus

  → Surfaces, polyhedra and the Euler characteristic, Homotopy and the fundamental group, Low-dimensional topology: 3- and 4-manifolds

• Triangles on a ball

  → Non-Euclidean geometry: spherical and hyperbolic, Differential geometry of curves and surfaces, Riemannian geometry

• Will the walker return?

  → Markov chains, Stochastic processes, Random structures: walks, percolation and random geometry

• Why do planets move on ellipses?

  → Classical mechanics, The geometry of spacetime: special and general relativity, Symplectic geometry and topology

• Loops around a hole

  → Homotopy and the fundamental group, Complex analysis, Algebraic topology

• How sharply does a road bend?

  → Differential geometry of curves and surfaces, Riemannian geometry, The geometry of spacetime: special and general relativity

• Arrows that compose

  → Categories, Functors

7. Website screenshots

8. Verification results

• Lean: build succeeded with leanprover/lean4:v4.35.0 on 2026-10-29; 3666 declarations, 0 using sorry; 349 exercises elaborate with sorry placeholders.
• Python: 368 of 368 experiments ran and passed their tests; pytest 5993 passed, 0 failed (Python 3.10.12, 2026-10-29).
• Human review: none yet. See the verification page.

9. Accessibility overview

• Semantic landmarks, a skip link, visible focus styles and keyboard operation of every interactive exploration (no drag-and-drop is required).
• Mathematics is rendered with KaTeX including MathML output for assistive technologies.
• Colour is never the only carrier of meaning: modes, statuses and feedback also use text and icons. Light and dark themes; reduced-motion preferences are respected.
• Feedback regions use live announcements; exercises accept regional numerals (e.g. Eastern Arabic or Devanagari digits).
• Known gaps: no formal accessibility audit has been carried out, and the interactive diagrams have not been tested with screen-reader users.

10. Internationalisation overview

• Six demonstration interface languages spanning several language families, scripts and both writing directions: English, Spanish, Arabic (right-to-left), Hindi (Devanagari), Simplified Chinese and Swahili.
• Only English is canonical. All other translations are machine-generated drafts, labelled as such, and none has been reviewed. The interface is translated; of the lessons, only the first (Collections) has been translated so far. In other languages, untranslated lessons are offered in English and marked "EN".
• A machine-readable language registry (BCP 47 tags, scripts, direction, status) and a registry of every UN member state with its official or de facto languages are included, with uncertain entries flagged for review.
• Six demonstration locales are not global coverage. That remains a long-term goal.

11. Known limitations

• Every topic in the map now has a first-draft lesson, but all lessons were drafted with AI assistance and none has been reviewed by a human mathematician or teacher. At the higher levels many central theorems are stated with references or proved only in outline; each lesson says which.
• Formal sections formalise what each lesson cites — often a key lemma, special case or definition rather than the headline theorem — and say precisely what is and is not formalised. Lessons from Grade 9 onwards build on Mathlib, which does not yet contain some of the mathematics taught. Lean exercises are solved locally or in the public Lean web editor, not inside the site.
• Some widgets are still missing (for example box plots, tree diagrams, directed graphs and a grid robot for young children); lessons use static figures there.
• Python runs in the browser via Pyodide, which downloads several megabytes on first use and needs a reasonably modern browser.
• Progress tracking is local to one browser by design; there are no accounts or cross-device sync.

12. Areas requiring human review

1. Mathematical accuracy of every lesson, trail, exercise and solution — especially definitions, theorem statements and proofs.
2. Pedagogy and age-appropriateness, particularly of the K–2 and Grades 3–5 lessons.
3. Historical claims in the "History and global context" sections.
4. All translations and the mathematical terminology glossaries.
5. The country and language registries, especially entries marked as needing review.
6. The curriculum map: topic placement, levels and prerequisite edges.

The Lumenary is an independent project and implies no institutional endorsement.