General topic

Stream: new members

[alex chan]

Hi, I have some general and some weird question

1) In what language lean carnel karnel written in ?? Like in c or c++
2) Any plans for Lean 5 ??
3) If Lean 5 Kernal and other things like syntax, libs written in Zig or Rust , will that be helpful like in performance
speedup ??
4) As lean is programming language can it be used for creating API's or blockchain ??
5) Lean4 with GPT-4 or similar latest models ??

[Johan Commelin]

1) Lean 3 is written mostly in C++. Lean 4 is written mostly in Lean 4.
2) No.
3) No plans for Lean 5, but Lean 4 is quite a high-performance language.
4) Yes.
5) Yes.

[alex chan]

Johan Commelin said:

1) Lean 3 is written mostly in C++. Lean 4 is written mostly in Lean 4.
2) No.
3) No plans for Lean 5, but Lean 4 is quite a high-performance language.
4) Yes.
5) Yes.

oo wow. Any project for blockchain on Lean 4 ??

[Johan Commelin]

I don't know

[Mario Carneiro]

@alex chan https://github.com/starkware-libs/formal-proofs is a project for formally verifying programs that run on the blockchain, by @Jeremy Avigad and StarkWare (a paper about it is on arXiv), but it is in lean 3, not lean 4. I am not aware of any major crypto / blockchain projects in lean 4 yet but I'm sure they will come eventually.

[alex chan]

That's wonderful, I will check it out.

[alex chan]

Any project regarding GPT4 / AutoGPT integration with Lean ??
If AutoGPT proves theorem on itself if given correct definition or theorem name which is not on mathlib ??

[Patrick Massot]

Search for sagredo on this website.

[alex chan]

sure, will do

[alex chan]

(deleted)

[alex chan]

(deleted)

[alex chan]

(deleted)

[alex chan]

How to close this chat ??

[alex chan]

I can't see any options for it.