Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry

The thirteen books of Euclid’s Elements

Thomas Little Heath et al · 1956

Earlier work this paper cites.

Plane geometry theorem proving using forward chaining

Arthur J Nevins · 1975

Earlier work this paper cites.

On the decision problem and the mechanization of theorem proving in elementary geometry

Wu Wen-Tsün · 1978

Earlier work this paper cites.

AUTOMATH, a language for mathematics

Nicolaas Govert de Bruijn · 1983

Earlier work this paper cites.

Proving elementary geometry theorems using wu’s algorithm

Shang-Ching Chou · 1984

Earlier work this paper cites.

Using gröbner bases to reason about geometry problems

Deepak Kapur · 1986

Earlier work this paper cites.

On zeros of algebraic equations–an application of ritt principle

Wenjun Wu · 1986

Earlier work this paper cites.

An introduction to wu’s method for mechanical theorem proving in geometry

Shang-Ching Chou · 1988

Earlier work this paper cites.

A refutational approach to geometry theorem proving

Deepak Kapur · 1988

Cited alongside, same era.

Visual reasoning in geometry theorem proving

Michelle Y. Kim · 1989

Cited alongside, same era.

Automated production of traditional proofs in solid geometry

Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang · 1995

Cited alongside, same era.

Realization of a geometry-theorem proving machine

H. Gelernter · 1995

Cited alongside, same era.

Reasoning about geometric problems using an elimination method

Dongming Wang · 1995

Cited alongside, same era.

Probabilistic verification of elementary geometry statements

Giuseppa Carr‘a Ferro, Giovanni Gallo, and Rosario Gennaro · 1997

Cited alongside, same era.

A formal system for euclid’s elements

Jeremy Avigad, Edward Dean, and John Mumma · 2009

Later among the works it cites.

An introduction to java geometry expert – (extended abstract)

Z. Ye, S.C. Chou, and X.S. Gao · 2011

Later among the works it cites.

Barycentric coordinates in olympiad geometry

Max Schindler and Evan Chen · 2012

Later among the works it cites.

Dealing with degeneracies in automated theorem proving in geometry

Zoltán Kovács, Tomas Recio, Luis F Tabera, and M Pilar Vélez · 2021

Later among the works it cites.

How can it be feasible to find proofs?

W. T. Gowers · 2024

Closest in time.

Open source prover in the attic

Original

Zoltán Kovács and Alexander Vujic · 2024

Closest in time.