The axiomatic details of Lean.

Stream: general

[Juho Kupiainen]

Does anyone have any suggestions for how I might go about studying the axiomatic details of Lean? I'm aware of the main.pdf at https://github.com/digama0/lean-type-theory/releases but.. what is the large arrangement of weird looking symbols in section 2 supposed to mean? Also, the paper says that type checking in Lean is undecidable. Does this mean that Lean might not be able to check some proofs?

[Keeley Hoek]

@Mario Carneiro is the author of that pdf. He also happens to be superhuman, so he'll probably be right over... :)

[Floris van Doorn]

what is the large arrangement of weird looking symbols in section 2 supposed to mean?

You will have to be a bit more specific, there are a large number of symbols in section 2. Do you mean the first displayed formula in section 2.1 (after "following grammar:")? That is Backus[-Naur|normal] form

[Floris van Doorn]

Many of the other displayed formulas are typing/inference rules: if all the conditions above the line hold, then the condition below the line holds.

[Floris van Doorn]

Also, the paper says that type checking in Lean is undecidable. Does this mean that Lean might not be able to check some proofs?

There are indeed proofs in the type theory that are not accepted by the Lean kernel. However, you should note that:

• You can always give a bit more information in your proof to help the type-checker along, so that it can verify your proof
• This is incredibly rare. I have never encountered this myself, and I don't know of any case in mathlib where we have to give this extra information to Lean (but maybe it has happened once or twice).

[Kevin Buzzard]

Is this about things like the pathological example of non-transitivity of definitional equality in the reference manual? Yeah, I have never seen anything like this happening "in real life". Leo is good ;-)

[Chris Hughes]

I think it happens quite a lot with acc.rec. I also think this is more or less the only place it comes up in practice.

[Mario Carneiro]

The main place it shows up in practice is that definitions by well founded recursion should result in definitional equalities in principle, but in practice you usually only get a propositional equality