Can Gödel's incompleteness theorem be proved in lean4?

Stream: mathlib4

[Planck Anderson]

Can Gödel's incompleteness theorem be proved in lean4?

[Planck Anderson]

Gödel's incompleteness theorem is a foundational result in mathematical logic. Since Lean 4 is a powerful proof assistant based on type theory, I'm curious whether it's possible to formalize and prove this theorem within Lean 4's framework. Can Gödel's incompleteness theorem be proved in Lean 4?

[Jireh Loreaux]

Please don't cross-post.

[Planck Anderson]

I'm trying to understand whether Gödel's incompleteness theorem can be fully formalized in Lean from a theoretical perspective. I’ve seen some work on formalizing the consistency of ZF in Lean, which made me wonder: is it possible, in principle, to formalize Gödel’s incompleteness theorems in Lean? Specifically, can the necessary components such as encoding of syntax, arithmetization of syntax, and fixed-point constructions (like the statement “sub(n, n, 17)”) be implemented in Lean’s framework? I'd appreciate insights on whether this has been done or what the main theoretical challenges are.

[Planck Anderson]

sorry I will delete it

[Jireh Loreaux]

it's okay, I've moved them all into this thread

[Weiyi Wang]

Is the 6th problem on https://leanprover-community.github.io/100.html the one you wanted?

[Brad S]

I don't have much understanding of how it works, but this project has a formalization of Gödel's incompleteness theorems.

https://formalizedformallogic.github.io/Book/first_order/goedel1.html

[Planck Anderson]

Thanks a lot! it is exactly this one