Feasibility of DAG extraction and Proof Compression in Lean

Stream: general

[ta-32]

Hello. I'm just getting started learning Lean, and had a random thought about the feasibility of extracting proof graphs from Lean code or merging or compressing Lean proofs.

https://en.wikipedia.org/wiki/Proof_compression

Even though I realize this is a very hard problem, ny insight on the topic would be appreciated.

[Quang Dao]

If you are happy with computational compression (i.e. the compression may fail to preserve soundness of a theorem up to some very small error, say 2^{-128}), then you can apply what's known as a SNARK (succinct non-interactive argument of knowledge) to compress Lean proofs. The new proof is essentially claiming "I know a Lean proof for this Lean theorem," and can be as short as a few hundred bytes. See this paper for more info

[ta-32]

Interesting! Thanks for the link.

[Jz Pan]

Quang Dao said:

the compression may fail to preserve soundness of a theorem up to some very small error, say 2^{-128}

Why will it fail? Hash collision?

[Quang Dao]

Essentially yes. Some SNARKs also rely on computational assumptions, so we also take into account, say, the probability of breaking discrete log for a given bound on running time

[Alex Meiburg]

(minor quibble) I think all SNARKs rely on some computational assumptions, at the very least "P != NP", otherwise the hash collision can be brute forced. But there are additional cryptographic assumptions I guess