[puffoflogic]

It's not clear to me that model theory has much to say about Lean; do you have any resources on this? plato.stanford.edu does hedge that while modern model theory focuses on first-order logic, there's a broader sense of model theory which can be used to study even natural languages. But if you try to study type theory as natural language statements you aren't going to get much out of it. Going about it that way, the models you'll come up with are going to be of the form "doing some formal symbol manipulation X has certain formal symbol results Y" which will be neither illuminating nor useful. I did find an abstract[0] which claims that model theory has historical roots in type theory but I'm doubtful I have any way to access it.

[0] https://www.cambridge.org/core/journals/bulletin-of-symbolic...

[auggierose]

First you have to see that the tutorial uses Lean basically as a blackbox. All that is needed is that you can express proofs in it, that applying lean to proofs yields lean theorems, that proofs are enumerable, and that Lean is powerful enough to express the collatz conjecture and the halting problem. So you can replace Lean by any other such blackbox B, for example B = (first-order logic + ZFC), and the argument in the tutorial goes the same way. Therefore type theory or not is not an issue here.

What IS an issue is that to fully explain what "express the collatz conjecture in B" means, you need model theory. You are right, type theory often doesn't come with model theoretic semantics, but it can be done in a natural way even for type theories.

The paper you are referencing is on sci-hub, by the way: http://sci-hub.wf/10.1017/S1079898600010568