English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This is the first paper in a series of work we have accomplished over thepast three years. In this paper, we have constructed a consistent formal planegeometry system. This will serve as a crucial bridge between IMO-level planegeometry challenges and readable AI automated reasoning. Within this formalframework, we have been able to seamlessly integrate modern AI models with ourformal system. AI is now capable of providing deductive reasoning solutions toIMO-level plane geometry problems, just like handling other natural languages,and these proofs are readable, traceable, and verifiable. We propose thegeometry formalization theory (GFT) to guide the development of the geometryformal system. Based on the GFT, we have established the FormalGeo, whichconsists of 88 geometric predicates and 196 theorems. It can represent,validate, and solve IMO-level geometry problems. we also have crafted the FGPS(formal geometry problem solver) in Python. It serves as both an interactiveassistant for verifying problem-solving processes and an automated problemsolver. We've annotated the formalgeo7k and formalgeo-imo datasets. The formercontains 6,981 (expand to 133,818 through data augmentation) geometry problems,while the latter includes 18 (expand to 2,627 and continuously increasing)IMO-level challenging geometry problems. All annotated problems includedetailed formal language descriptions and solutions. Implementation of theformal system and experiments validate the correctness and utility of the GFT.The backward depth-first search method only yields a 2.42% problem-solvingfailure rate, and we can incorporate deep learning techniques to achieve lowerone. The source code of FGPS and datasets are available athttps://github.com/BitSecret/FGPS.

FormalGeo: The First Step Toward Human-like IMO-level Geometric Automated Reasoning