mmforge
Finds a theorem that pays for an axiom it does not need, then builds the proof that removes the dependence and checks it.
What it does
Two halves of one loop. The analysis finds a theorem that pays for an axiom it does not need; the construction writes the replacement proof and checks it.
pip install mmforge mmforge reach set.mm --axiom ax-ac mmforge impact set.mm --axiom ax-ac --top 40 mmforge domination set.mm mmforge conformance set.mm
The finding it came from
set.mm is 47,621 theorems deep. 583 of them reach the axiom of choice and three actually invoke it — everything else inherits. 418 of the 583 inherit through exactly one step, which means each has a single place where the dependence could be removed.
The lower half of that table is measure theory, which has no business being
there. difelsiga says a sigma-algebra is closed under set
difference; below it sit 64 results including Bayes' theorem.
Repairs do not add up
Fixing one statement frees a count that is not the count you get when you
fix it alongside the others. fimact alone frees one theorem; in the
stack it frees fourteen. Every per-repair figure this reports is a lower bound,
and it says so rather than adding them for you.
How it works
- Install it
pip install mmforge. One entry point, seven subcommands. - Measure
mmforge reach set.mm --axiom ax-acshows what reaches an axiom and how each one gets there.impactranks theorems by how many others a repair would free. - Build the repairThe construction half writes the replacement proof and verifies it. Eight of the repairs that came out of this loop are merged upstream.
What it finds
ac2, axac3 and zfac. Everything else inherits.difelsiga says a sigma-algebra is closed under set difference. Below it sit 64 results including Bayes' theorem, none of which needs choice.fimact alone frees one theorem; in the stack it frees fourteen. Every per-repair figure is a lower bound and the tool says so rather than summing them.$j 'avoids' directives and checks the declarations are still true.Specifications
| Install | pip install mmforge |
|---|---|
| Version | 0.2.0 |
| License | MIT |
| Reads | Metamath databases |
| Upstream | 8 pull requests merged into set.mm |
| Source | vince-gonzalez/mmforge |
Questions
- Do I need a Metamath install?
- For verification, yes. The analysis reads the database directly.
- Is this only about the axiom of choice?
- No — that is the worked example.
--axiomtakes whichever constant you want to trace.