Proofs

ProofWiki: good stuff here - finally having time to appreciate it, now that I basically know how to deploy an equivalent cloud service. All this needs is an automated theorem prover feature... maybe it's there, but I don't see it.

Anyway, all in line with further studies in demonstrating why people are boring.

Demonstrate a machine that can beat humans in an argument.

Step one... learn how to encode human arguments in a machine-readable language.

Well, at least as of today, I've managed to link up my understandings of LaTeX, and Haskell, via mathematical proofs and the functionality of Agda.

What did you think... of course I'm not interested in math for math's sake... pooh pooh...

Also of interest, some other stuff in automated theorem solving, automated theorem checking, and proof assistance:

Mizar system
Metamath

Annoying as it seems (either my own ignorance of the counterexample, or the fact that) there is no standard, like an ISO, for computer readable mathematical proofs.

HOL (subject: higher-order logic) also looks like it needs serious looking into - for my education, on how this stuff is currently treated by the world at large. Ah, time is always short. (A family member of HOL being Isabelle, and Haskabelle.Haskabelle by the HOL-ML-Haskell project group.)

I already kinda know Haskell - but OCaML seems to have been more closely associated with this sort of software in the past. Also checking out HaskHOL. Much to learn.

Proof Assistants - history, ideas, and future