Formal and computational evidence
On this page · Permalink · Source line 323
FRESH SOURCE CHECKING AND BOUNDED EXACT REPLAY The current pinned Lean replay passed for all 115 indexed theorem declarations and eight modules. The permitted axiom union is propext, Classical.choice, and Quot.sound. No project axiom or admitted proof occurs in the maintained source.
The complete exact scientific replay also passed. Its finite domains are recorded in the claim-coverage appendix and in the emitted run manifest. The degree-profile checker counts 278 functions on zero through three inputs. The small-oracle construction suite counts 276 functions on one through three inputs. The two zero-arity functions explain the difference. Those totals are not added together as disjoint evidence.
The package retains historical failures as historical records. Current source compilation, kernel replay, finite computation, source integrity, and PDF rendering each establish a different kind of fact.