Elektrine lite

← Feed

@rntz@recurse.social

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.