A 4AP-free permutation of the positive integers

Source: arxiv:2609.12780, url:https://github.com/boonsuan/4ap Authors: Boon Suan Ho Status: verified Main declarations: FourAP.exists_fourAPFree_positive_permutation Tags: additive-combinatorics, arithmetic-progressions, Erdos-problem-196, permutations MSC: 11B25, 05D10