A sharp 5/8 bound for Erdős Problem 865

Source: url:https://github.com/mrricky22/erdos-865-lean Authors: Ricky Cipollini Status: verified Main declarations: Erdos865.erdos865_upper_bound, Erdos865.sharpness Tags: additive-combinatorics, erdos-problems, sum-free-sets, combinatorics MSC: 11B75, 11B13