“制造业”这个词百分百被用错了，导致了百分百的误解。
真正该用的词是“机械文明”，相对于今天的“赛博文明
”。
机械文明时代，最大的就业红利其实不是叫大学生脱下长衫打螺丝（反正诸位长...
©2010-2025 Purasbar Ver3.0
[手機版]
[桌面版]
除非另有聲明，本站採用知識共享署名-相同方式共享 3.0 Unported許可協議進行許可。
大学生就业为什么这么难呢？(转自知乎李劼）“制造业”这个词百分百被用错了，导致了百分百的误解。
真正该用的词是“机械文明”，相对于今天的“赛博文明 ”。 机械文明时代，最大的就业红利其实不是叫大学生脱下长衫打螺丝（反正诸位长... |
回覆：lean4的简单程序import Mathlib.Data.Real.Basic
-- 一个稍复杂一些的例子，使用intro策略给各个假设命名 theorem my_lemma : ∀ x y ε : ℝ,... |
回覆：lean4的简单程序两横线 -- 是注释， 井号后面一般是关键字，比如说#check，#eval
|
回覆：魔力赏集市是一个好东西，但是魔力赏不是以前那些一元购，淘宝的淘必中，京东的夺宝，也是类似的方式，也是沉迷者太多，国家最后整治了
|
回覆：如果被父母知道，我是为了获得去鬼屋做NPC的资格才坚持去健身房锻炼的加油
只要你确实能做好这个工作，父母最终还是会理解的 |
回覆：lean4的简单程序-- 一部分换行丢了。。重新发
-- 两横线后面是注释 -- 计算#eval 12+12 -- 计算，结果是24 -- 类型检查 #check 3 -- 类型检查，结果是ℕ... |
lean4的简单程序-- 两横线后面是注释-- 计算#eval 12+12 -- 计算，结果是24
-- 类型检查 def f (x :ℕ) := x + 3 #check f -- 类型检... |
回覆：lean4教程回复 @啊啊是谁都对：有的，git clone https://github.com/leanprover-community/mathematics_in_lean.git下载mathematics...
|
回覆：【记录】俄乌战争2024/4/22~4/28：俄军攻占奥切列季涅，威胁红军城和顿河君士坦丁罗夫卡
|
lean4教程https://leanprover-community.github.io/mathematics_in_lean/
这个教程是关于如何用lean4和mathlib4做数学的 https... |