looking forward to this!

[JeffreySarnoff]

(not an issue)

[lucaferranti]

thank you very much, I am very happy to hear that!

The package is at its early days, but there's already a short tutorial demoing the main functionalities: https://lucaferranti.github.io/GeometricTheoremProver.jl/dev/write_statements/

That should be ok for the writing hypothesis thesis part (of course feedback is always welcome if something is unclear). The part about the prover is very minimal and a few features (how to pass arbitrary coordinates, how to extract intermediate steps) are still undocumented. Improving the documentation of the current features is my main goal for this week.

I'll probably open a roadmap issue and smaller enhancement issues, but as a teaser here are a few features coming up (hopefuly) during this spring

• export to latex/markdown/similar
• plotting
• implement area method: this is nice because opposed to Ritt-Wu method, it gives a (kind of) human readable proof.

I'll keep the issue open for now to remind me to keep working on this! 😄

[JeffreySarnoff]

I am hoping for a triangle or simplex primitive. Something to smarten-up with some of the known Euclidean theorems and to fatten-up with access to prover-aware special points and their dual constructs. If you do want triangle, then segment orientation becomes handy .. and so to the availability of vertex angles. For that, I'd be interested in framing Angle as measure of a constraint and segment orientation as a "more generalized Angle (or triplet, or n-let)".