== Quote from retard (r...@tard.com.invalid)'s article > I really love digitalmars.D because this is one of the few places where > 99% of the community has zero experience with other languages, other > paradigms (non-imperative), automatic theorem provers, or anything not > related to D. There's a whole choir against theorem proving now. The > funniest thing is that none of you seem to have any clue about how those > programs work. Has anyone except the almighty Andrei ever even downloaded > a theorem prover?
Does the Maxima computer algebra system count? It has a basic theorem prover built in, and I've played around with it a little. If this is how theorem provers work, then they have a long way to go.
