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.

[Matthew House]

I've reviewed this pretty thoroughly and found a few dozen issues with the basic read–verify pipeline. I've uploaded them as failing test cases to https://github.com/LegionMammal978/mm-verifier-tests/tree/eb4e2938d3d91c4edd104e2536e0549f48533a0a. (Anyone else wanting to test their verifier is free to use this repo.) There's also another bug with the Python bindings: when a proof is replaced in a database, it does not check that the proof does not refer to future labels.

The major soundness bugs are that it fails to check whether hypotheses are active, verify * fails to print a warning if a proof before the last contains an unknown step, and the Python bug I mentioned.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/26a9b719-bd99-49ef-a515-cae5473fbf7an%40googlegroups.com.