台灣正體 | 登錄 | 註冊

目前共有4篇帖子。內容轉換：不轉換▼

點擊	回復
116	3

lean4教程

初級魔法師四級

1樓發表于：2024-5-2 16:20

回復

https://leanprover-community.github.io/mathematics_in_lean/
这个教程是关于如何用lean4和mathlib4做数学的

这个教程是lean4语言本身的教程，更偏向对语言机制的介绍，不包含mathlib的使用

執行總編二十一級

2樓發表于：2024-5-2 17:26

回復

感觉使用lean4很像用计算机编程

	悄悄打开魔盒：回复 @啊啊是谁都对：有的，git clone https://github.com/leanprover-community/mathematics_in_lean.git下载mathematics_in_lean，在这个项目的目录下lake exe cache get就可以下载相应的依赖文件，然后在vscode里打开项目文件夹，在MIL子文件夹下就可以看到例子了
	2024-5-2 23:41 回復
	啊啊是谁都对：有无最简单的实例？
	2024-5-2 17:42 回復

回復帖子

本帖信息

點擊數：116

回複數：3

	【新功能】现在手机版发帖也可以上传图片了
	【公告】布拉斯侃吧（Purasbar）全站已启用HTTP/2访问以及TLS1.3加密
	【新功能】楼中楼功能已上线
	【公告】Purasbar http访问方式已关闭，从现在起只能通过https方式访问
	【新功能】现在可以直接在发帖框中粘贴图片啦！
	【新功能】搜索框提示功能上線了
	【公告】第十五次補丁包安裝完畢
	【公告】從現在開始，管理員將停止審批會員
	【公告】阿斯兰侃吧现在开始支持简繁混合搜索
	【公告】阿斯蘭侃吧啟用https訪問
	【公告】从今天开始，本站实行主题编号制
	【新功能】图片缩放功能上线了

	©2010-2024 Purasbar Ver2.0 ▲
	除非另有聲明，本站採用創用CC姓名標示-相同方式分享 3.0 Unported許可協議進行許可。