Johan Belinfante

Georgia Tech


Experience with computer-assisted reasoning in set theory

Thursday, January 29 at 4:30pm, Skiles 269




I will summarize my experience proving over a thousand theorems in set theory using Bill McCune's program Otter . I will also talk about my Mathematica program GOEDEL to convert expressions involving class-formation to a form suitable for use with Gödel's finite axiomatization of set theory.