Proof representation?

Stream: general

[Alex Sweeney]

I think I understand that Lean proofs are a sequence of dependent type theory statements rather than computing something or running an algorithm like many programming languages. I'm not super familiar with Lean or type theory, but surely the proof is expanded to eliminate the convenient language features and make it possible the kernel to check. Similar to how machine code is unreadable for humans but it's unambiguous to the CPU. What is the expanded representation for Lean proofs called and where can I read more about it?

Thank you

[Aaron Liu]

The process of expanding is called elaboration

[Aaron Liu]

not sure what the expanded version is called but they're represented as docs#Lean.Expr I think

[Chris Henson]

Have you already seen this page about the kernel?

[Siddhartha Gadgil]

In addition to the internal Expr representation, there is also an exporter to a format that can be checked by an external typechecker (and in practice is checked by more than one everyday).

[Kyle Miller]

If you #print a theorem you can see a pretty printed form of the "proof term" that is checked by the kernel.