Joshua Clune: A Formalized Reduction of Keller's Conjecture. CPP 2023: 90-101