# Discussion about getting rid of random reward bounties

[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:**

- Discussion about getting rid of random reward bounties -
**Brown**, 2020-09-24, 12:01- Discussion about getting rid of random reward bounties - , 2020-09-24, 14:35
- Discussion about getting rid of random reward bounties -
,
2020-09-24, 14:40
- Discussion about getting rid of random reward bounties -
**BlakeKeiller**, 2020-09-24, 19:53

- Discussion about getting rid of random reward bounties -
- Discussion about getting rid of random reward bounties -
**BlakeKeiller**, 2020-09-24, 19:54- Discussion about getting rid of random reward bounties -
,
2020-09-24, 20:27
- Discussion about getting rid of random reward bounties -
**BlakeKeiller**, 2020-09-26, 15:14

- Discussion about getting rid of random reward bounties -

- Discussion about getting rid of random reward bounties -
,
2020-09-24, 20:27