"Oh my god, it's such a big project, nobody should do it alone". It's very obvious, isn't it? 500+ pages of abstract proofs need to be expressed into some kind

"Oh my god, it's such a big project, nobody should do it alone". It's very obvious, isn't it? 500+ pages of abstract proofs need to be expressed into some kind of programming language. Not to mention, the worst case is that he doesn't even know what coq is, or have never used a programming language (probably just TeX, since he's mathematician) and will take him sometime to pick it up, and then learn how to express his idea using it, etc ... Look at the linux kernel we have right now, let's go back to early 90s, and should we tell Linus not to do it because it's so big? And did it end up Linus doing it all alone himself? Coq is certainly not a short term solution, but definitely a valid one if no one else wants to read his proof, and it's very important for him validate it. The reason I bring Coq up is that in general, I do feel proving things in maths is very much like writing a program in a programming language. Maybe the 500+ pages of proof is like a spaghetti code, refactoring might make it more readable, or more clear, so people are more likely to study it. Or the 500+ pages of proof is very elegantly constructed, just need someone to appreciate it. Coq can certain help in both cases. But then is it worth it for him to do it? That's really he's judgement call based on how important the proof is, what he see he can get out of this, etc. Remember that line from the article you quoted: "Fun ~enormous!"