Inspirations

A functional programming language and interactive theorem prover developed at Microsoft Research. Lean 4’s approach to dependent type theory and its growing mathlib library inspire MoonMath’s goal of making formal verification accessible to learners.

The community-driven mathematics library for Lean 4, demonstrating that large-scale formalized mathematics is practical and collaborative.

Tutorial resource showing how mathematical proofs translate to Lean, a direct inspiration for MoonMath’s interactive proof exploration.

The Fractal Geometry of Nature — the foundational work on fractals as a language for describing natural complexity, inspiring MoonMath’s visualization approach.

The iconic fractal demonstrating how simple iterative formulas produce infinite complexity — a core theme in MoonMath’s visual explorations.

Techniques for generating fractals (Sierpinski triangle, Barnsley fern, etc.) that MoonMath aims to make interactive.

Grant Sanderson’s visual approach to mathematics, showing that animation and interactivity transform abstract concepts into intuition.

Mathematical animation engine used by 3Blue1Brown, inspiring the visualization pipeline.

Rust web framework enabling SSR + WASM hydration, chosen for a pure-Rust stack.

Fast LaTeX math rendering, used server-side via katex-rs for pre-rendered math output.

Immediate-mode GUI in Rust, planned for interactive canvas and code editor with no JS dependency.

Static site generator whose content organization (TOML frontmatter, _index.md sections) inspired MoonMath’s content pipeline.

Modern typesetting system, planned for PDF export in later milestones.

Lean-to-LaTeX tooling, planned for the v0.5 milestone bridging formal proofs to rendered math.