Tuesday, April 30, 15:15, 7.527

István Szöllősi (Cluj)
Computer assisted proof of the tree module property for exceptional tame representations

Abstract:
We present a computational method used for explicitly describing and proving the so-called tree module property (or tree representations) in the case of Euclidean quivers. Recall that tree representations are indecomposable and can be exhibited using matrices involving only the elements 0 and 1, with the total number of ones being exactly d-1 (where d is the length of the module). Due to a result of Ringel the existence of tree representations is guaranteed when the module is exceptional (indecomposable and without self-extensions).

Tree representations may be given generally (via formulas describing the block matrices), but after the theoretical toolchain is in place, the process of writing the proofs quickly becomes cumbersome, time-consuming and error-prone if performed by a human. The formulas describing the matrices are obtained via "educated guesses" based on computer experimentation in the computer algebra software GAP (Groups, Algorithms and Programming) and a proof is written by our proof assistant software. The proof uses symbolic computation and structural induction, (once the required formulas are given). We have developed the proof assistant software in the functional programming language Clean, which takes a LaTeX file (containing the formulas defining the representations) as input and produces an output LaTeX document containing a complete proof, with the arithmetic operations on symbolic block matrices written in a detailed step-by-step manner, as if done "by hand". In this way one does not have to believe in the correctness of the implementation, because the complete proof is "on paper" and every single step may be crosschecked and verified by a human mathematician.

Using the novel method, we were able to give a complete and general list of tree representations corresponding to exceptional modules over the path algebra of the canonically oriented Euclidean quivers of type D˜_m and E˜₆. Moreover, all these representations remain valid over any base field, this fact answering an open question raised/suggested by Ringel.