### A surprising story of how a computer was taught to prove some theorems in finitely complete categories

Notes for the talk given at the 2021 Congress of South African Mathematical Society on 29 November. 1. Finitely complete categories A finitely complete category is a category that has finite products and equalizers (and hence, all finite limits). Not every category is finitely complete, but most categories of mathematical structures are. There is a representation theorem for finitely complete categories (Yoneda embedding), which allows to present any category as a full subcategory of a (larger) category of presheaves of sets, which is closed under all limits that exist in the category. This means that a lot of times, proving a theorem in a finitely complete category involving finite limits, reduces to proving the same theorem in the category of sets. For instance, the fact that the product of objects is commutative, up to a canonical isomorphism, can be deduced from the fact that the same is true for the cartesian product of sets. Or, the fact that the composite of two monomorphisms