Challenging Proofs By Mathematical Induction


Maintainer: Carsten Schürmann
Department of Computer Science
Yale University



This collection of challenging examples has been assembled for researchers who are working on inductive theorem provers for the purpose of provoding a body of test examples. The description of the example problems is purposely kept informal, in order not to intervene with the representation of a problem in a particular theorem prover.

Major contributions to this corpus have come from
  • Louise Dennis, University of Edinburgh
  • Dieter Hutter, DFKI
If you want to contribute to the corpus, please send mail to Carsten Schuermann. New additions will be annouced on the challenges mailing list. You may subscribe to the mailing list by sending email to with "subscribe challenge" in the body (the header might stay empty). Everybody is invited to submit challenges.

001 - Arithmetic Geometric Mean

  1. First Order Version of the Arithmetic/Geometric Mean
  2. Higher Order Version of the Arithmetic/Geometric Mean (Version 1)
  3. Higher Order Version of the Arithmetic/Geometric Mean (Version 2)

002 - Length of the joined list of two lists of even length is even

003 - A member of a list is a member of that list joined to another

004 - Rotate Length

  1. Rotate Length (Version I)
  2. Rotate Length (Version II)

005 - Binomial Theorems

  1. Binomial Theorems (Version I)
  2. Binomial Theorems (Version II)

006 - Two definition of Even are equivalent

007 - All numbers are odd or even

008 - Chinese Remainder Theorem

  1. Chinese Remainder Theorem (Version I)
  2. Chinese Remainder Theorem (Version II)
  3. Chinese Remainder Theorem (Higher-order)

009 - "Pete's Nasty Theorem"

010 - Quicksort

011 - Safety Lemma for Removing the head of an abstract list

012 - Safety Lemma for Prefix Operation

013 - Divide and Conquer

014 - Harald's Problem

015 - Paulson's Problem

016 - Quicksort verification

017 - Verifying Abstractions in Model Checking (revised)