I've been working on DeepMind's AlphaGeometry lately. My goal was to work out its logical foundations in order to generalize the system beyond Euclidean plane geometry and across different mathematical theories, while adding a layer of formal verification.
In this paper, we formalize the underlying logic and provide a mechanized proof of soundness using the Lean 4 theorem prover. This might appeal to those interested in neurosymbolic AI for theorem proving and automated reasoning. I'm happy to answer any questions.
Hi HN,
I've been working on DeepMind's AlphaGeometry lately. My goal was to work out its logical foundations in order to generalize the system beyond Euclidean plane geometry and across different mathematical theories, while adding a layer of formal verification. In this paper, we formalize the underlying logic and provide a mechanized proof of soundness using the Lean 4 theorem prover. This might appeal to those interested in neurosymbolic AI for theorem proving and automated reasoning. I'm happy to answer any questions.