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 https://github.com/ReedOei/Pecan and http://reedoei.com/pecan for more information about this software. The underlying motivation for this theorem prover is to automatically decide statements about Sturmian words (see https://en.wikipedia.org/wiki/Sturmian_word).
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 https://wiki.illinois.edu/wiki/display/IGLSP20/Building+a+Theorem+Prover and https://wiki.illinois.edu/wiki/display/IGLFA20/Pecan+-+an+automated+theorem+prover
MATH 347 and previous knowledge of automata is required. Students with significant experience in Python are preferred.