Metadata-Version: 2.4
Name: symave
Version: 0.2.3
Summary: Deterministic verification of European high school math axioms.
Project-URL: Homepage, https://gitlab.com/mzezulka/libraries/symave
Project-URL: Source, https://gitlab.com/mzezulka/libraries/symave
Project-URL: Issues, https://gitlab.com/mzezulka/libraries/symave/-/issues
License: MIT
License-File: LICENCE.txt
Classifier: Intended Audience :: Education
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Education
Classifier: Topic :: Scientific/Engineering :: Mathematics
Requires-Python: >=3.14
Requires-Dist: sympy
Provides-Extra: dev
Requires-Dist: bandit; extra == 'dev'
Requires-Dist: black; extra == 'dev'
Requires-Dist: hatch-vcs; extra == 'dev'
Requires-Dist: mutmut; extra == 'dev'
Requires-Dist: mypy; extra == 'dev'
Requires-Dist: pip-tools; extra == 'dev'
Requires-Dist: pytest-cov; extra == 'dev'
Requires-Dist: pytest>=7.0; extra == 'dev'
Requires-Dist: python-semantic-release; extra == 'dev'
Requires-Dist: ruff; extra == 'dev'
Description-Content-Type: text/markdown

# symave

`symave` stands for **SY**mbolic **MA**th **VE**rifier. 
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](https://openmath.org/). OpenMath is an excellent starting point but may not be sufficient for various reasons:
- geometric and combinatorial concepts have limited representation [[Labre, 2026]](https://arxiv.org/abs/2602.17826)
- 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]](https://arxiv.org/abs/2602.17826)
- even though OpenMath [strives to be unambiguous](https://openmath.org/technical/), 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](https://openmath.org/cd/) that group related concepts together; further, referencing across the ontology is possible; however, tagging or any other indexing is limited

## Install

```bash
pip install symave

```

## Usage

```python
from symave import get_verifier

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

```

## Development

Requires [Hatch](https://hatch.pypa.io/).

```bash
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
```