6
$\begingroup$

I'm aware of Lean's type theory. Did the type theory of lean change at all as we moved to Lean 4? Are there any references to this?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
2
$\begingroup$

Some things changed but the type theory stayed exactly the same, so e.g. https://github.com/digama0/lean-type-theory/releases/tag/v1.0 is still a valid reference (edit: apparently this is not completely correct -- see Sebastian's comment below)

Improve this answer
$\endgroup$
3
  • 6
    $\begingroup$ It is not exactly the same, the major additions are primitive projections, eta for structures, and primitive mutual inductive types. My PhD thesis, which should be available some time next month, gives more details. $\endgroup$
    – Sebastian Ullrich
    Commented May 4, 2023 at 20:01
  • 2
    $\begingroup$ @SebastianUllrich Given that Kevin’s answer is slightly wrong, it wouldn’t be bad for you to make your own short answer with what you just said. It also wouldn’t hurt to add a line about if the changes are conservative (in that you can still prove the same theorems) and if there is an automatic way to translate Lean 3 kernel-level proofs to Lean 4 (which I assume there is given the early work on the mathlib port which translated the kernel-level proofs). $\endgroup$
    – Jason Rute
    Commented May 5, 2023 at 10:35
  • $\begingroup$ @SebastianUllrich How can I read your thesis when it is complete? Are these the only additions that were made? And how would these affect me working in Lean? $\endgroup$
    – Alex Byard
    Commented May 12, 2023 at 13:12
5
$\begingroup$

As already commented by Sebastian Ullrich, there are a few small changes to the Lean 4 kernel, detailed in his PhD thesis. Now, that it is done (and has been for a few months), I want to make sure it gets the attention it deserves. The details on the kernel are in Section 3.2.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you, Jason. Would you recommend I read his entire thesis? $\endgroup$
    – Alex Byard
    Commented Oct 27, 2023 at 0:56
  • 1
    $\begingroup$ @AlexByard I’m not sure I’ve ever recommended one read a thesis, and TBH I haven’t read Sebastian’s. That being said, it looks, from the bits I’ve skimmed, well organized, so at least skimming it would give you a lot of information. $\endgroup$
    – Jason Rute
    Commented Oct 27, 2023 at 1:02

Not the answer you're looking for? Browse other questions tagged or ask your own question.