Just dropping in to say it's nice to see somebody actually try to work through the proof, and it gives one confidence that the proof at least isn't complete nonsense (which is helpful given the few details provided about the process behind it).

With the Erdős proof, OpenAI added perspectives from working mathematicians that gave some context -- hope something like that appears for this one eventually.