Understanding the Kernel

Stream: IMO-grand-challenge

[Marijn Stollenga]

I find the IMO challenge a very interesting idea; to understand how to apply search algorithms though I would like to understand what happens in Lean on the lowest level possible. Is there a good resource explaining the minimal kernel in lean perhaps?

[Johan Commelin]

Have you seen Mario's thesis?

[Johan Commelin]

That explains Lean's type theory in detail. Is that the kind of resource you want?

[Bryan Gin-ge Chen]

There's a series of links on the community webpage here: https://leanprover-community.github.io/learn.html#more-on-foundations

[Marijn Stollenga]

Johan Commelin said:

Have you seen Mario's thesis?

Ah yeah I think i've seen that. It's interesting but a bit I would like something closer to the programming level if that makes sense?

[Marijn Stollenga]

Bryan Gin-ge Chen said:

There's a series of links on the community webpage here: https://leanprover-community.github.io/learn.html#more-on-foundations

That sounds interesting indeed!

[Daniel Selsam]

@Marijn Stollenga depending on the level of detail you are looking for, I would recommend reading one of the reference kernels. I wrote one in Haskell many years ago (https://github.com/leanprover/tc) and there are others floating around in other languages.

[Marijn Stollenga]

I saw you Haskell paper, so funny XD. I saw that it kind of abruptly ended? Is everything there, I guess I should learn Haskell.
Maybe a good project is to port that to some other language (Zig perhaps).