lean-axiom-provenance

Find out what a Lean 4 project actually rests on, and why. Reports every theorem reaching a sorry anywhere upstream, everything settled by native_decide rather than the kernel, and the shortest path from any declaration to any axiom with each hop labelled a statement dependency or a proof dependency. Use when the user asks what their proof depends on, whether a sorry is inherited from a dependency, why a theorem…