Discussion about getting rid of random reward bounties

by , Thursday, September 24, 2020, 20:27 (437 days ago) @ BlakeKeiller

[barakeel] One idea would be to implement some compression schemes: using lemma sharing, term sharing by making definitions and possibly beta-reducing the proof term. This does not have to be a modification to the kernel but that would be useful tool. Most proofs generated by ATPs are too big to be translated in a direct manner. For example, today I reduced a 600MB to 11MB proof by introducing lemmas and I hope I can reduce it below the size limit for a block by introducing definitions for commonly occuring subterms .

Complete thread:

 RSS Feed of thread

powered by my little forum