A from-scratch TypeScript DDAR geometry proof-checker (deductive database + algebraic reasoning, the symbolic method behind AlphaGeometry) that verifies olympiad proof steps against several resampled figures, plus the interactive geometry course built on it.

Companion page for "Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery." A curated four-axis index covering MWPs, LLMs and reasoning models, multimodal geometry, Lean theorem proving, and verified discovery (FunSearch, AlphaEvolve, Erdős problems).