My "Patterns of Resemblance Arithmetical Library (PORAL)" is, in a formal sense, one of the most sophisticated pieces of software ever written: the ordinals it

My "Patterns of Resemblance Arithmetical Library (PORAL)" is, in a formal sense, one of the most sophisticated pieces of software ever written: the ordinals it can perform arithmetic upon are so large, they require nontrivial fragments of set theory just to prove they're really ordinals. Some of the algorithms implemented in this library were recently printed in "Archive for Mathematical Logic", a hardcore logic journal. Github: https://github.com/semitrivial/poral https://github.com/semitrivial/poral