I then push everything back up to the master Github repository. The blueprint will take quite some time (about half an hour) to rebuild, but eventually it does, and the dependency graph (which Blueprint has for some reason decided to rearrange a bit) now shows “ruzsa-nonneg” in green

靠。

cpp 都没这么慢

（胡说，我就是 cpp）

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 能搜出来证明过程。

???

也不冲突