This repository contains Krympa, a tool for minimizing equational proofs by combining subproofs generated by automatic theorem provers.

For a detailed description of Krympa and the proof-minimization approach, see the accompanying paper:

Tao’s Equational Proof Challenge Accepted

• Python 3
• A Unix environment (Linux)

The repository provides multiple Krympa binaries for different proof settings:

• ./krympa — base tool
• ./krympa_bs — big-step + small-step problems
• ./krympa_sa — small-step + abstracted problems
• ./krympa_ba — big-step + abstracted problems

All binaries expose the same CLI interface:

krympa <command> <input-file>

Commands executed in the pipeline:

run_vampire → collect → shorten → minimize

All execution is performed from the shell directory:

cd shell

./run <timeout>

Example:

./run 2700

This runs the benchmarking pipeline on the full benchmark set.

Each Proofs*.lean file is converted into a corresponding benchmark folder (e.g. benchmarks/input7/), which contains multiple individual benchmark problems. The timeout is applied to each individual benchmark problem, not to the entire folder or the full benchmark suite. Problems are processed sequentially.

The console output shows only high-level progress information. Detailed logs for each benchmark folder are written to:

../benchmarks/output_logs/

Each Proofs*.lean file produces a corresponding log file in that directory.

First generate the corresponding inputs:

python3 ../python/generate_input.py ../benchmarks/Proofs11.lean

Then run:

./run_one ../benchmarks/input11/Equation650_implies_Equation448.p

run and run_one accept an optional binary argument.

./run_one <input-file> <krympa-binary>
./run <timeout> <krympa-binary>

python3 ../python/summarize.py ../benchmarks/output_logs

python3 ../python/tolean.py /path/to/output_proof_file

Example:

python3 ../python/tolean.py ../benchmarks/output/proof_Equation650_implies_Equation448.out

• The run script performs full benchmarking and may take significant time.
• Benchmark execution is currently sequential; parallel execution will be added soon.
• Output logs and minimized proofs are written automatically.
• All Krympa binaries are interchangeable in the pipeline.

If you want to propose changes, fixes, or new features:

1. Open an issue describing your suggestion or bug.
2. Submit a pull request referencing the issue.
3. All contributions will be reviewed before merging.

Direct forks or redistribution of modified versions are not allowed.