symave 0.2.3

Deterministic verification of European high school math axioms.

symave

symave stands for SYmbolic MAth VErifier. This project is intended to be used as a library for deterministic user lemma verification, as an alternative to statistical approaches that are in some contexts unacceptable, namely in education. This library focuses on rudimentary axioms, statements and propositions present in a typical high school curriculum.

What it does

Given a mathematical symbol (e.g., integer1:factorof) and a student expression, symave returns whether the expression satisfies the symbol's definition.

Symbols are defined in a Knowledge Base (KB) based on OpenMath. OpenMath is an excellent starting point but may not be sufficient for various reasons:

• geometric and combinatorial concepts have limited representation [Labre, 2026]
• OpenMath is a standard with multiple encodings (XML, binary, Content MathML); the format of mathematical expressions across content dictionaries is heterogeneous, which poses challenges for consistent indexing [Labre, 2026]
• even though OpenMath strives to be unambiguous, it does not provide an API (that's not what the project aims to achieve, anyway)
• OpenMath categorization is strictly hierarchical and achieved through content dictionaries that group related concepts together; further, referencing across the ontology is possible; however, tagging or any other indexing is limited

Install

pip install symave

Usage

from symave import get_verifier

verifier = get_verifier("integer1:factorof")
verifier.verify(params={"n": 6}, expression="3")  # True

Development

Requires Hatch.

hatch run test      # run test suite
hatch run lint      # format + lint + type check
hatch run sec       # security scan
hatch run kb-serve  # browse the Knowledge Base at http://localhost:8787