Checking axioms with leanchecker

Stream: lean4

[Eric Wieser]

Could leanchecker learn a flag to forbid axioms beside the standard axioms (especially sorry)? This seems like it would be helpful to resolve some of the issues in the DeepSeek prover thread, and would also be a nice sanity check for Mathlib

[GasStationManager]

As mentioned in the other thread, https://github.com/GasStationManager/SafeVerify
was something I wrote a while back based on leanchecker, that additionally throws error if axioms other than the standard ones were used.
See the function checkAxioms in https://github.com/GasStationManager/SafeVerify/blob/main/Main.lean
which is then called on line 119.

[Thomas Zhu]

@GasStationManager your function uses CollectAxioms.collect, which in #lean4 > #print axioms does not report sorry is shown to be unreliable. In particular it will return the empty list for the example shown there.

[GasStationManager]

Interesting... I've not looked at this deeply, but do we know that this is due to a bug in CollectAxioms.collect, or elsewhere? Is this fixed in a later version of Lean?