Hacker News Reader

They’re not, but they’re spectacularly good at spotting dumb errors that humans are spectacularly bad at spotting.

Me, I still haven’t got my head around how to prove something on a computer, but the principle is sound. Theoretically one could build the proof as some form of literate program.

View on HN

A computer just does symbolic manipulation according to a list of rules (axioms) and the human/programmer specifies which sequence of symbolic manipulations to apply and then the computer simply states whether or not the specified manipulations transform the theorem in to the truth symbol.

http://us.metamath.org/mpegif/mmcomplex.html

(Warning: I've never actually done much of this before so some details might be wrong.)

I have done some, thanks for pointing to that page!

Here's a prettier version for most people (the "mpegif" version uses GIFs for math symbols, which works everywhere but doesn't look at nice):

http://us.metamath.org/mpeuni/mmcomplex.html

Reply on news.ycombinator.com