The objective of ChatMath is to develop a language model for the
presentation, verification, generation, and communication of mathematical
knowledge using natural and formal languages with advanced
techniques of machine learning and automated reasoning. The rationality
of the project may be seen from the outcome of case studies on the
retrieval of geometric information and the generation of geometric
theorems from image data. For example, the following proposition
can be automatically generated from the diagram image
and be formally proved to be a true theorem, the Simson Theorem.
Xiaoyu Chen, Dan Song, and Dongming Wang: Automated Generation of Geometric Theorems from Images of Diagrams. Annals of Mathematics and Artificial Intelligence 74 (2015) 333-358.
Dan Song, Dongming Wang, and Xiaoyu Chen: Retrieving Geometric Information from Images: The Case of Hand-drawn Diagrams. Data Mining and Knowledge Discovery 31(4) (2017) 934-971.