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
![[*]](themes/default/images/complete_thread.png "Open whole thread")
- 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 -
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 -
,
2020-09-24, 20:27