Krympa
Proof minimization tool for equational reasoning
Krympa is a research tool for minimizing equational proofs by combining subproofs generated by automated theorem provers.
It provides a reproducible pipeline for running provers, collecting intermediate proofs, shortening them, and producing minimized results.
The project supports benchmarking workflows and utilities for converting proof outputs into formats suitable for further formalization.
Repository:
github.com/kondylidou/Krympa