Mechanizing Gödel's Incompleteness Theorems and Provability Logic

We mechanized proof of Gödel’s first and second incompleteness theorems, Solovay’s arithmetical completeness theorem of $\mathbf{G}\mathbf{L}$, and related results in the Lean 4 theorem prover.