Paul is currently developing the GCL ANSI Test Suite, a comprehensive set of ANSI Common Lisp standards compliance tests. All developers of Common Lisp implementations are encouraged to run the tests and send feedback to dietz AT dls.net. The tests are currently (December 2004) about 85% done. The next part to be done is to finish testing of the Environments section. After that, System Construction and the Reader will be tested, followed by a sweep through the standard to fill in parts that were missed (such as long form method combination definition.)
Paul has also put together a random test generator for exercising lisp compilers. It is included in the gcl ansi-tests suite, but runs separately from the test suite proper. Anyone making a significant change in a Common Lisp compiler is encouraged to run this tester immediately; it has often quickly found bugs in new optimizations.
For what it's worth: nothing says that pages should be listed in one topic and one topic only: that something is a Theorem Prover doesn't disqualify it from being related to AI. Just a minor point (and feel free to delete this text) but I thought I'd mention it - dan