Online interactive first-order logic theorem prover with Tarski axiom set for Euclidean geometry.
Embed several aspects of predicate functor logic directly into the GUI. Expressed axiom schema as a monad.
Leverage Elm type system to formally verify the design’s correctness. Explore Zipper data structure capability as an alternative method to identify generated data instead of wrapping inside the Random monad.
Roadmap
Monad to geometrically graph the current state of theorems
High level axioms / Birkhoff's axioms / First order axiomization of the reals.