This chapter presents some recent explorations we have made in the domain of learning to solve geometry proof problems. The background of these explorations consisted of two research programs: one investigating general principles of learning and the other investigating the nature of problem-solving skill in geometry. We have been conducting these two programs relatively independently since about 1976, but both programs have used versions of Anderson's (1976) ACT production system as a computational formalism. Our investigations of learning have included a discussion of general assumptions about learning and design issues (Anderson, Kline, & Beasley, 1980) and an analysis of prototype formation (Anderson, Kline, & Beasley, 1979). Our studies of geometry problem solving have included an analysis of forms of knowledge required for successful performance (Greeno, 1978), a discussion of goal representation (Greeno, 1976), and a discussion of schematic knowledge involved in planning (Greeno, Magone, & Chaiklin, 1979). The knowledge required to solve proof problems is moderately complex, but because its structure has been studied in some detail, it serves as a feasible target for a theoretical analysis of learning. In our investigations, we have found ways to extend both the previous analysis of learning and the previous analysis of problem-solving skill significantly.