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

阶段	个已绘入地图的主题	课程已上线
幼儿园至二年级	9	Collections
三至五年级	15	Sets
六至八年级	21	Functions, Integers
九至十二年级	25	Composition
本科低年级	21	—
本科高年级	34	—
研究生一年级	33	—
研究路径	11	—

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. Set theory and category theory progressions

Earlier mathematics emphasises sets; category theory is introduced gradually as a structural language for higher mathematics. Neither replaces the other. The topics currently mapped in each progression are:

5. Representative lessons

1. 一组对象 · 幼儿园至二年级 · 5 Lean · 1 Python

   分类、属于，还有令人惊奇的空盒子——集合最初的想法。

2. Sets · 三至五年级 · 7 Lean · 1 Python

   Membership, subsets, unions and intersections — the language almost all of mathematics is written in.

3. Integers · 六至八年级 · 8 Lean · 3 Python

   Numbers below zero, the opposites that cancel them, and a proof of why negative times negative is positive.

4. Functions · 六至八年级 · 6 Lean · 1 Python

   Rules that give exactly one output for every input — drawn as arrows, built from ordered pairs, and sorted into injective, surjective and bijective.

5. Composition · 九至十二年级 · 8 Lean · 1 Python

   Doing one function and then another — why order matters, why brackets don't, and how this simple idea opens the door to category theory.

6. Wonder Trail demonstrations

• Boxes inside boxes

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

• How many infinities?

  → Countability and Cantor's diagonal argument

• 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

• Arrows that compose

  → Categories, Functors

7. Website screenshots

8. Verification results

• Lean: build succeeded with leanprover/lean4:v4.35.0 on 2026-10-28; 88 declarations, 0 using sorry; 7 exercises elaborate with sorry placeholders.
• Python: 12 of 12 experiments ran and passed their tests; pytest 571 passed, 0 failed (Python 3.10.12, 2026-10-28).
• 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. Untranslated content falls back to English with a visible notice and the correct language attribute.
• 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

• Only five lessons and seven Wonder Trails exist; every other topic in the map is planned, not written.
• The formal library uses core Lean 4 only; Mathlib integration is planned. Lean exercises are solved locally or in the public Lean web editor, not inside the site.
• 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.