2026-09-12 21:36 UTC
Do any proof assistants expose a way to get the "trust base" of a given theorem (excluding the checker itself)? This means:
1. All definitions transitively used by the theorem statement. (A mistake in a definition means you've proved the wrong theorem!)
2. Any axioms/postulates; anything proved by sorry/admit/etc.
Is this standard? If not, why not? Seems essential for proof review.
Replies (0)
No replies.