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.