I didn’t know him that well, but could see him being the kind of person who wants to avoid attention. He was happy to spend some time explaining the problem to me and why it was interesting and difficult.
I'm sorry, I don't get it. What are you suggesting to be the motivation to remain anonymous in this case?
Prevents embarrassment if it turns out one’s idea is wrong, I suppose.
The person in question formalized the entire proof in Coq, which certifies its correctness.
To me, that makes your conjecture very unlikely to be true...
I didn't mean to suggest anything. I was just interested in whether they thought that remaining anonymous was in keeping with their ex-colleagues character. Written communication is hard!