Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic

AI use, as the source states it

“The entire Agda development, comprising approximately 50,000 lines and containing no postulates, was produced through interaction with Claude; the author did not write any Agda code.”

Model: Claude, as stated