Announcing brianna — Metamath verifier with Python bindings

[Nick Davis]

I'd like to share an early project: brianna, a Metamath verifier in C++ with a metamath.exe-style CLI and Python bindings.

Repo: https://gitlab.com/marcusucubi/brianna

I wanted to load .mm files, verify proofs, and inspect statements from Python without reimplementing a verifier. brianna is a C++ engine with a small Python package on top. Other Python Metamath work exists (e.g. metamath-py, mmverify.py); brianna's angle is a fast C++ core, familiar CLI (read / show / verify), and the same engine exposed to Python.

Currently:
• CLI with wildcard verify (*, ?)
• Proof tree / Lemmon-style display
• Python: load, verify, find statements, format proofs
• Optional PyQt6 database browser
• Passes metamath-test (140/140 on --small-only)

import brianna

db = brianna.Database()
db.load("mm/hol.mm")
summary = brianna.verify_all(db)
print(summary.succeeded, "of", summary.total, "proofs verified")

Build: CMake 3.20+, C++17, Qt 6 Core; Python 3.10+ for bindings.

I developed this with substantial help from Grok (https://grok.com). Testing and design choices are mine; Grok helped heavily with implementation.

This is early software — feedback on correctness, API, and docs would be very welcome.