To make yourself familiar with the system CERES and the additional tools
we have prepared the following examples:
Very simple examples just to get a glimpse of how cut-elimination is done
with CERES and how the workflow with the auxiliary tools molds.
Instances of a proof schema which gives exponential cut-free proves. These
examples clearly justify and suggest the use of computer aided
A convenient sized proof of a simple but practical mathematical statement.
A larger proof of a still simple but more practical mathematical statement.
A huge formal proof of a significant number-theoretical mathematical statement with a complex indirect topological proof.
A second-order proof, showing that the least number principle implies the
fact that every number greater than 1 has a prime divisor.