이 책이 채택한 해법은 컴퓨터 형식증명 시스템이다. 즉 학생이 작성한 증명에 오류가 있는지를 컴퓨터가 판별해 줌으로써, 학생들이 엄격한 수학적 증명에 대한 훈련을 받도록 하는 것이다. 필자는 2009년 봄부터 컴퓨터 논리 시스템 Proofmood의 개발을 시작하여 중학교 영재 학생들 및 학부 학생들을 대상으로 논리 교육에 활용해 왔다. 초기에는 주로 명제논리를 이용한 논리퍼즐 문제를 다루어 많은 학생들의 흥미를 끌수 있었다.