Chaitin's incompleteness theorem

Stream: computer science

[Matt Diamond]

Apologies if this is a naive question, but is Chaitin's incompleteness theorem something that could eventually be proved in Lean? It seems to require a sort of meta-proving ability that Lean doesn't have right now.

[Aaron Liu]

it looks like it's saying something about the strength of formal systems

[Aaron Liu]

you would have to formalize formal systems and formalize the statement of complexity within those formal systems within Lean

[Matt Diamond]

yeah, it might be something for the FormalizedFormalLogic project to tackle

[Matt Diamond]

creating a method of generating all valid proofs and then extracting the description of the string under analysis from a given proof might be tricky

though maybe the existence of the enumerator and extraction methods could be an assumption