lambdasgr's comments

Location: Texas

Remote: OK

Willing to relocation: yes

Resume/CV: www.linkedin.com/in/ritchie-cai-33536a10

E-mail: ritchiecai at r2labs.org

Technologies: Clojure, C/C++, CUDA, Python, Linux/Unix, Bash, Matlab, Git, Verilog

That's odd, I was able to compile both bazel and tensorflow from source since early spring 2016 on RHEL 6.5 (not that it was straight forward ...), so it should work for centOS as well.

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

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.

LaTeX. Here are some custom latex classes I uses for different purpose. Some are created by me, some are I get from elsewhere: https://github.com/malloc82/latex_classes