FormalGeo
The International Mathematical Olympiad (IMO) is perhaps the most celebrated mental competition in the world and as such is among the ultimate grand challenges for Artificial Intelligence (AI). We have constructed a complete and compatible formal plane geometry system called FormalGeo. This will serve as a crucial bridge between IMO-level plane geometry challenges and readable AI automated reasoning.
With FormalGeo in place, we have been able to seamlessly integrate modern AI models with our formal system. Within this formal framework, AI is now capable of providing deductive reasoning solutions to IMO-level plane geometry problems, just like handling other natural languages, and these proofs are readable, traceable, and verifiable.
Regarding the research achievements in geometric formalization, we have divided them into five parts: geometry formalization theory, geometry formal system, formal geometric problem solver, formal geometric problem dataset, and AI-assisted geometric problem solving.
Regarding the geometry formalization theory, you can read the original paper:
FormalGeo: The First Step Toward Human-like IMO-level Geometric Automated Reasoning
Regarding the solver, you can learn about these projects:
FormalGeo: Formal representation and solving for Euclidean plane geometry problems.
FGPS: Formal geometric problem solver based on FormalGeo.
New formal system and datasets will be published in these projects:
AI-assisted formal geometric problem solving:
FGeoDRL: Formal Geometric problem solving based on deep reinforcement learning.
FormalGeo adopts open source as its growth strategy. We welcome anyone to contribute to FormalGeo, even if you are new to open source. FormalGeo is currently maintained by the FormalGeo Development Team and supported by Geometric Cognitive Reasoning Group .