Theory Compressor

v0.4 — Compressor + HTML Proof Graph
Compressor
Post-proof theorem set minimization. Announced externally as “Pruner,” renamed to Compressor internally to avoid ambiguity with the Pick-and-Prune algorithm central to the prover.
Tests each theorem for redundancy: if it can be re-derived from the remaining set, it is eliminated. Two phases — dependency discovery via independent Logic Blocks, then greedy elimination sorted by redundancy.
Results: Peano 64→17 theorems (73%), Gauss 20→12 (40%). Adds ~1s to a 407s pipeline.
HTML Proof Graph Visualization
Navigable HTML proof graph with chapter-based structure, theorem cross-referencing, and full derivation provenance. Extensive debugging pass covering variable renaming, anchor resolution, and proof origin handling.
A fully verified version will follow once the proof graph verifier is integrated.​​​​​​​​​​​​​​​​