A distinct covering system of congruences is a finite collection of arithmetic progressions to distinct moduli \[ a_i \bmod m_i, 1 < m_1 < m_2 < \cdots < m_k \] whose union is the integers. Answering a question of Erdős, I have shown that the least modulus $m_1$ of a distinct covering system of congruences is at most $10^{16}$. I will describe aspects of the proof, which involves the theory of smooth numbers and a relative form of the Lovász local lemma.