Our synthetic Euclidean Geometry proof assistant is now open for public contributions! We created this together as a class in my Build Your Own Proof Assistant course this semester. Please give it a spin and consider contributing! https://github.com/nicegeo/nicegeo Some features: - Dependent-type-theory-based proof kernel - Synthetic Euclidean geometry layer (axiomatization of System E) with elaboration exhaustively tested - Tactic-based interactive proofs - Holes, bidirectional type checking, and unification - Proof state management - Custom tactic framework in OCaml - Pretty-printing and error reporting - Kind error messages - Standard library (Euclib) for Euclidean geometry - VSCode IDE plugin with many novel usability features - Some geometry-specific proof automation What's next: - Interactive visual proofs - Tabular proofs - More geometry-specific & advanced automation - Better support for user-written automation (e.g., a tactic language) - Stronger IDE integration - Expansions to Euclib Please see our GitHub issues for more! Our proof assistant is MIT licensed. Please see our contributor's guide if you would like to contribute. We especially welcome contributions addressing any of our open GitHub issues! https://github.com/nicegeo/nicegeo?tab=contributing-ov-file This was a very impressive collaboration of about 20 students from many different backgrounds, who all came together for a semester to build something real. Everything from the domain to the design philosophy to the kernel to the automation was built from scratch collaboratively!