Major: Mathematics and Philosophy Year: Senior
Hometown: Canal Fulton, OH
Honors: MCS Dean's List
Project title: "Intelligible Collapse of Formal Proofs"
Type of Support: SURF 2009, SURG 2010
When did you become involved in undergraduate research at CMU? My second semester of sophomore year.
How did you find your mentor? Wilfried Sieg was my logic professor sophomore year and he offered me a position with his research group, the AProS project. I worked on improving the automated theorem prover developed by the group. To continue my research, Dr. Sieg proposed I apply for a SURF to work with him over the summer and explore possible abbreviations for making the formal proofs produced by theorem prover structurally transparent and more intelligible to human beings.
How has your idea/project evolved through the academic years? My project is an on-going process. I continue to work with Dr. Sieg and the AProS project, making advances toward improving the search algorithm for the automated theorem prover and making the generated proofs more intelligible. Right now we are in the process of obtaining an automated proof of the Cantor-Bernstein theorem, a theorem of axiomatic set theory expressing that two sets are of the same size if each set is of lesser or equal size than the other. My SURF and SURG results will play an important role in trying to get such a complex formal proof to be readable.
What successes or difficulties have you encountered in this project or others? It is difficult pursuing original research in general. When trying to solve a problem for a homework assignment or a class project, you can usually find resources online or in textbooks that can guide you to the correct solution. When running with ideas of your own, you have to rely on what you think is right and not what others have already established as being right.
If you could summarize your experience in one word, what would it be? Impelling