感觉不用mathlib这语言没法玩啊

这也难怪 不用 std 我也不会 cpp

（但是用mathlib就好卡…）

优化不行…..（x

不幸的是，Desai 不能让设备发出低于 2000Hz 的声音，因此《一闪一闪亮晶晶》音符都向上移动了好几个八度。

dissy dissy

哭了。

Immersive Math (🔥 Score: 151+ in 2 hours)

Link: https://readhacker.news/s/67E9E
Comments: https://readhacker.news/c/67E9E

赞

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

笑死