Esther is a work-in-progress, proof-of-concept automated theorem proof assistant based on Homotopy Type Theory.

Acknowledgements

• Arend, Lean, Coq and Agda, for introducing me to world of formalised mathematics and proof assistants.
• Nikita Tonsky's clj-kondo, for an inspiration for a logo.

Community

Matrix: you can find us on Matrix on #esther:matrix.org.