Notes on Laver Tables

Abstract

We present some new lower bound estimates for certain numbers in Laver table theory and introduce several related structures of interest.

Thanks the AI for math team of Peking University, Jiang Jiedong, Zhang Zhiyuan and Chen Leheng so much, for using Lean 4 to formalize the main theorem of this work, and finding many typos during their formalization