Theoremica

Inspiration

One of the most difficult parts of taking a math class in university is learning all of the proofs. Sometimes studying for tests can get tedious, so instead of practicing proofs on paper, we decided to make a fun visual proof assistant which can both autonomously correct our proofs and help us have a bit more fun doing them!

What it does

Theoremica uses visual code blocks for users to construct proofs both more easily and more rigorously. It converts those code blocks into the proof assistant language Lean and runs the Lean script to verify if the proof is mathematically correct or not. Many problems in MATH 240 are available on Theoremica as well as a "daily challenge" math problem.

How we built it

We developed Theoremica as a web app with a front end in HTML, CSS and JavaScript and a backend in python using Flask. The translation of code blocks to Lean script were done using the Gumloop API.

Challenges we ran into

One of the biggest challenges we ran into was unexpectedly harmonizing the Flask and JavaScript, as we had multiple bugs that set us back a while. Another challenge was finding the proper balance between speed and precision for the LLM implementation in Gumloop in order to get the optimal user experience.

Accomplishments that we're proud of

We are proud of producing a functional, useful product that is fun to play with. Although it is by no means a finished product, we believe that it has the potential to make math students' lives much easier by gamifying one of the dullest parts of studying and we will look into bettering this product even further.

What we learned

One of the things that we learned is that even though perseverance is necessary to accomplish our goals, sometimes taking a step back and even trying a fresh start is the right move to get past obstacles even though it sometimes hurts to do away with the things we have worked so hard on.

What's next for Theoremica

Built With

• gumloop
• javascript
• python