Discussion about getting rid of random reward bounties
As you suggest, it's already possible to use definitions and lemmas to compress proofs. It's just that it's up to the author to do it. Hopefully someone will make automated tools to help do this.
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 -
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