Is type checking in "Ideal Lean" computably enumerable?

Question

There are actually two type theoretic foundations of Lean given in Mario Carneiro's master's thesis. They are the same, except for how definitional equality is treated:

• “algorithmic” definitional equality is weaker and is closer to what is actually implemented in Lean. This version of definition equality is not transitive, but it is decidable, and hence type checking is decidable.
• "ideal" definitional equality is stronger. This version of definition equality is transitive, but not decidable.

The question: Is type checking in the idealized type-theory of Lean at least computably enumerable (a.k.a. recursively enumerable, a.k.a. semi-decidable)?

---

Hat tip: Pierre-Marie Pédrot asked this question in a comment to "Are there computable functions which can't be expressed in Lean?". The answer to that question (and likely others on this website) basically assume that type checking in Lean is computably enumerable. While that is true for the algorithmic definitional equality version of Lean (which is honestly probably the version people mean when they ask questions about Lean), it isn't clear it holds of the more idealized foundation.

---

I suspect the answer to my question is likely yes, since Ideal Lean is a type theory given by a finite list of type-theoretic rules. I assume the language the rules are written in is itself computably enumerable and that checking each rule is decidable. If so, it is enough then to search for a derivation which derives the appropriate type checking judgement.

However, I feel someone more familiar with Lean's idealized type theory can answer this with certainty.

Answer 1

Yes. The reasons are as you stated: A typing judgment is a statement about finite objects (expressions and contexts), and because typing judgments are inductively defined, every judgment has a "proof", a tree of rule applications leading to the judgment, and those proofs are also necessarily finite. Finally, the typing rules are computable, in the sense that you can determine whether a specific rule application is in fact a valid application of that rule - this boils down to checking that a substitution is performed correctly, replacing the metavariables in the axiom specification with the specific substitutions used in this particular application.

Thus, it suffices to just enumerate all possible derivations and throw out everything that is not a valid derivation. For each derivation you can look at the last line of the derivation and if that is your desired sequent then you are done. There are infinitely many derivations to check, but that's why it is computably enumerable and not just computable.

(This is all pure proof theory, nothing specific to lean is used in this argument.)