We believe the Lean 3 theorem prover’s success is primarily due to its extensibility capabilities and metaprogramming framework [6]. However, users cannot
modify many parts of the system without changing Lean 3 source code written
in C++. Another issue is that many proof automation metaprograms are not
competitive with similar proof automation implemented in programming languages with an efficient compiler such as C++ and OCaml. The primary source
of inefficiency in Lean 3 metaprograms is the virtual machine interpretation
overhead.
Lean 4 is a reimplementation of the Lean theorem prover in Lean itself4
.
It is an extensible theorem prover and an efficient programming language. The
new compiler produces C code, and users can now implement efficient proof automation in Lean, compile it into efficient C code, and load it as a plugin. In
Lean 4, users can access all internal data structures used to implement Lean
by merely importing the Lean package

笑死

#今天又看了啥 #academic #LLM #ICLR
唐杰的 PPT: The ChatGLM’s Road to AGI
https://keg.cs.tsinghua.edu.cn/jietang/publications/iclr24-chatglm-en-v2.pdf

开幕雷击⚡️

万能的 ring

ring 门

易得 --> AI 能搜出来证明过程。

???

也不冲突

太多了。。。。