The minimal version of the Prolog source code is only 360 bytes. This is of course hardly readable; there is also the standard distribution of lean, which comes with a rudimentary user interface and some test examples. It is distributed as a shell archive (see information on getting the source code).
In addition, there is a lean tableau-based prover available for propositional modal logics, called ModLeanTAP.
Jens Otten from TU Darmstadt has developed a lean connection-based prover leanCoP. There is also a version for intuitionistic first-order logics, called ileanTAP.
The paper is 20 pages long; it contains a sketch of a proof for lean's correctness and completeness, and a brief historical survey on tableau-based provers (BibTeX entry).
lean is written in SICStus Prolog, but it works as well under Quintus Prolog, and it can be easily ported to other Prolog systems (for example Eclipse and SWI Prolog).
Problems taken from the TPTP library can be converted into lean syntax (using the program tptp2x, which is part of the TPTP distribution).
Finally, if should you do something interesting with lean, please inform us. This could be modifying or extending the program, applying it to some domain, or whatever. We appreciate feedback.