Hacker News Reader

Comment by lambdasgr | Hacker News Reader

He probably should try to use Coq proof assistant. If Coq proves his proof, then mostly like it's correct. Of course, it's easier to say than to do, not a trivial work, and he's the only one who can do it, since he's the only one who can understand the proof.

But if he indeed able to write the entire proof in Coq, then I'm sure at that point, his proof will be much cleaner as well.

Then again, this will never happen.

View on HN

That is like a complete no-go. It took something like 6 years[0] to formalize the proof of Feit-Thomson, one of the first "long" proofs in group theory, and that was done by experts who understood both Coq and the proof. In the time it would take him to write the proof in Coq, dozens of mathematicians could learn the theory and independently verify it.

[0] http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/

"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!"

Writing a program is exactly the same thing as proving a mathematical statement. This is an extremely cool and deep result. Start with the Church-Turing thesis and go from there.

Except in Math we accept duck-typed functions to prove our results. Advanced math is not fully rigorous and often has mistakes.

Sure. But no dozens of mathematicians are stepping up to take the roughly half a year (and novice-like zen) he anticipates it requiring to understand the proof. So if he wants it to happen: do a lecture series, or programmatize the proof, or write an expanded walkthrough book series to explain it in less condensed form. Or just complain to new scientist and see if any new folks decide to pick up the torch, I guess.

Reply on news.ycombinator.com