Michael Beeson's Research

Tarski Formalization Project: Results

We used OTTER to find proofs of the theorems in Tarskian geometry in the first nine chapters of Szmielew's development in Part I of Metamathematische Methoden in der Geometrie. Those theorems include the four unsolved challenge problems from Quaife's 1992 book, and the verification of Hilbert's axioms. Of the approximately 200 theorems, we proved 57% mechanically and without strategies (except for a good choice of settings), and by the use of the subformula strategy we increased that to 76%. By using lemma adjunction and hint injection, which depend on starting with a book proof, we achieved a 100% success rate. We have discussed the contents of the book, and the definition of "hard", "simple", and "elementary" theorem (in terms of proof length), on this page. Please refer to that page for a discussion of the theorems mentioned by name in the table below. Here is a table showing the hard theorems from the entire book, with the number of steps in the proof(s) that we obtained. A paired number like $(99,921)$ indicates a proof found mechanically using the subformula strategy, of length 99 and found in 921 seconds. The last column gives the number of steps taken explicitly in the book proof. Not counting the lines with a question mark, we have 1900 Otter steps corresponding to 465 book steps, giving a de Bruijn factor (the ratio of the two).