Hacker News new | past | comments | ask | show | jobs | submit login

Oh, it can capture everything. I believe that. It's just that it relies on volunteers to actually do the work of formalizing advanced theories. It has some pretty darn advanced stuff already, like complex numbers. But there's also a huge amount of research-level mathematics which nobody's gotten around to coding in the Metamath formalism yet. This is the same issue discussed in the video: with millions of dollars and a full time team, you could get something like the proof of Fermat's last theorem in there, but its not there yet.

Metamath has a proof of Prime Number Theorem. Its coverage of advanced mathematics is pretty much as good as any.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact