Developing Pecan

Faculty Member

Philipp Hieronymi

Project Image

In the Spring 2020 IGL project "Building a theorem prover" and the Fall 2020 IGL project "Pecan - an automated theorem prover" we built an automated theorem prover called "Pecan". See and for more information about this software. The underlying motivation for this theorem prover is to automatically decide statements about Sturmian words (see

In Spring 2021 we will continue to improve Pecan and increase its functionality.

Newcomers are welcome. For more details about what has been done previously, see and

Team Meetings


Project Difficulty


Undergrad Prerequisites

MATH 347 and previous knowledge of automata is required. Students with significant experience in Python are preferred.