This is an overview of systems implementing "mathematics in the computer" as compiled by Freek Wiedijk. Similar information can be found at:
This is the version that is sorted by category. There also are versions without samples and in black-on-white text. And there also are versions of this list grouped by alphabet, by implementation language, by most common interaction mode, by the logic that is supported, and by the size of the effort. Finally, there is a short explanation of the various fields in this database.
This information is still incomplete and there probably are some errors in it. I would appreciate it if people would help me correct and complete it.
First Order Prover