We will talk about our recent result settling an old conjecture of Paul Erdős: we prove that the density of any measurable planar set avoiding unit distances can not reach 1/4. Our solution is heavily computer-aided, and uses ideas from linear programming, graph theory, and harmonic analysis. This question is related to the famous Hadwiger-Nelson problem, and some of its variants. We will conclude by mentioning some still-unsettled conjectures that might be approached with our machinery. A joint work of Gergely Ambrus, Adrián Csiszárik, Máté Matolcsi, Dániel Varga and Pál Zsámboki. The talk is self-contained.