3 ms·
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 t
by moomin 8y ago
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.
- chess93 8y agoA 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 http://us.metamath.org/mpegif/mmcomplex.html (Warning: I've never actually done much of this before so some details might be wrong.)
- dwheeler 8y agoI 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 http://us.metamath.org/mpeuni/mmcomplex.html