Lean4 Release Date

Stream: lean4

[Shubhra Mishra]

Hi! I was trying to figure out when Lean4 was released. From here, it seems like September 7, 2023 is when Lean4 was officially released. However, there are a lot of versions before 4.0.0. Does this mean that all versions before it (despite not being official) were publicly available? I'm trying to figure out where or not there is any possibility that GPT-3.5 was trained on Lean4 syntax, which would only be possible if the pre official release versions were publicly available before early 2022.

[James Gallicchio]

I think there's been publicly available versions since at least 2019?

[James Gallicchio]

(and the syntax hasn't changed too much since at least 2020)

[Kyle Miller]

The first public beta release was January 2021 I believe. I don't remember exactly when it was announced, but there were some talks at Lean Together 2021 about it.

I have a Lean 4 github repo with a bit of code from back then.

[Kyle Miller]

Hmm, I just remembered that Reid Barton did the 2020 Advent of Code in Lean 4. I don't remember when Lean first became available.

[Kim Morrison]

Re: GPT 3.5, yes, it has certainly seen some Lean 4 syntax, but likely very little outside the compiler itself.

[Mario Carneiro]

Found the initial message: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.204.20is.20going.20public/near/164159039, so lean4 was first made public on 2019 April 24

[Mario Carneiro]

The first public talk about lean 4 (after this point and linking to the repo rather than just talking about plans) was at PLDI 2020 > https://www.youtube.com/watch?v=TgHISG-81wM

[Shubhra Mishra]

Ahh, I see. Thank you very much, James, Kyle, Scott, and Mario!