Proof Path Theory

Download original file

Read the formatted document

1 # Evidence layout
2 
3 Current formal run: `formal_1.7.0/`.
4 Current integrated release run: `release_1.7.0/`.
5 Current development failures/corrections: `development_1.7.0/`.
6 
7 `lean/` and the earlier versioned directories retain historical runs. They
8 must not be reported as fresh verification of modified sources. The new run
9 uses pinned cached imports and Lean's own kernel; it is not an independent
10 validator or a full rebuild of Mathlib. Source hashes bind each record to the
11 files actually checked.

Back to source controls