{"id":"arxiv/2609.13780","url":"https://arxiv.org/abs/2609.13780","tags":["cs.LO","math.LO"],"score":0,"title":"Mechanizing Gödel's Incompleteness Theorems and Provability Logic","domain":"cs.LO","source":"arxiv","authors":["Shogo Saitou","Mashu Noguchi"],"reviews":0,"subject":"cs.LO","summary":"We mechanized proof of Gödel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \\mathbf{GL}, and related results in the Lean 4 theorem prover.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-09-12","reactions":{}}