This folder contains the three source batch trees that back the benchmark and proved-result views.
These trees are labeled Foundational, Applied, and Abstract to match the paper’s three-domain taxonomy.
These are the source artifacts behind the cleaner top-level ../MathlibLemma/ presentation view.
Some smaller follow-up directories were moved out to ../supplementary_experiments/explicit_necessary_conditions_ablation/ so that the main source trees here remain focused on the core benchmark story.
The clearest starting point for most readers is:
../MathlibLemma/
That directory presents the main results in benchmark form rather than in raw batch form. The current folder is the archival/raw batch view behind it.
This folder contains two complementary views of the same main-result body.
- The aggregated benchmark/result view:
../MathlibLemma/Benchmark/../MathlibLemma/Proved/ByModel/../MathlibLemma/Proved/ProofLibrary/
- The original source batch trees, renamed here for readability:
FoundationalAppliedAbstract
The aggregated view is for readability. The raw batch trees are for traceability.
The benchmark corresponds to the main source-batch pool after filtering out trivial compilable statements. That yields:
4028non-trivial compilable Lean statements
This is the benchmark-facing subset emphasized by the paper.
The original batch directories preserve the historical structure of the main project, including generated lemmas, corrected statements, compilable statements, solved outputs, and related quality-check directories. They are kept here so that the benchmark presentation remains auditable back to the underlying source artifacts.