I have a program that generates incidence theorems in projective geometry. The following slides from my talk at SiCGT23 in Kranjska Gora explain the program and the notation that it uses to output theorems.