Some caveats: This is only really designed to work for set.mm. In particular it bakes in two assumptions which are correct for set.mm but not necessarily for other databases:
It only supports compressed proofs, and will panic on normal mode proofs, and possibly panic or give the wrong result on packed proofs.
It assumes that axioms are marked with the ax- prefix, meaning that definitions are ignored, but also nonstandardly named axioms.
Based on a request at https://github.com/metamath/set.mm/issues/3150#issuecomment-1529101901 . This generates a list of the axioms used by every statement in set.mm, like so:
It takes about 200ms to generate the file.
Some caveats: This is only really designed to work for set.mm. In particular it bakes in two assumptions which are correct for set.mm but not necessarily for other databases:
ax-prefix, meaning that definitions are ignored, but also nonstandardly named axioms.