Kim Morrison uses Claude and Codex to formalize Alpöge's Erdős unit-distance disproof in Lean

Oh and Kim Morrison used Claude + Aristotle + Codex to formalize the negation of the Erdos unit distance conjecture: https://github.com/kim-em/erdos-unit-distance

It's nice to see that this was built on top of PNT+; so despite the fact that we haven't been able to upstream it to Mathlib (the Residue Theorem we have in PNT+ is just for rectangles, and Mathlib will want a much more general version...), it's still useful in other applications!...