There are currently 4 posts.
Font size: Small - 100% (Default)▼  Content converter: No conversion▼
 
Clicks Replies
1972 3
lean4教程
悄悄打开魔盒
大魔导士 十七级
Reply
Floor 1 Posted at: 5/2/24 16:20
https://leanprover-community.github.io/mathematics_in_lean/
这个教程是关于如何用lean4和mathlib4做数学的


https://leanprover.github.io/theorem_proving_in_lean4/

这个教程是lean4语言本身的教程，更偏向对语言机制的介绍，不包含mathlib的使用
啊啊是谁都对
总编 二十四级
Reply
Floor 2 Posted at: 5/2/24 17:26
感觉使用lean4很像用计算机编程
 
啊啊是谁都对: 有无最简单的实例？
  5/2/24 17:42 Reply
悄悄打开魔盒: 回复 @啊啊是谁都对：有的，git clone https://github.com/leanprover-community/mathematics_in_lean.git下载mathematics_in_lean，在这个项目的目录下lake exe cache get就可以下载相应的依赖文件，然后在vscode里打开项目文件夹，在MIL子文件夹下就可以看到例子了
  5/2/24 23:41 Reply
Reply the post
Content:
User: You are currently anonymous.
Captcha:
Unclear? Try another one.
(Shortcut key: Ctrl+Enter)
Post Information
Clicks: 1972 Replies: 3
Author: 悄悄打开魔盒
Last reply: 悄悄打开魔盒
Last reply time: 5/2/24 23:41
Announcements
 【新功能】现在手机版发帖也可以上传图片了
【公告】布拉斯侃吧（Purasbar）全站已启用HTTP/2访问以及TLS1.3加密
【新功能】楼中楼功能已上线
【公告】Purasbar http访问方式已关闭，从现在起只能通过https方式访问
【新功能】现在可以直接在发帖框中粘贴图片啦！
【新功能】搜索框提示功能上線了
【公告】第十五次補丁包安裝完畢
【公告】從現在開始，管理員將停止審批會員
【公告】阿斯兰侃吧现在开始支持简繁混合搜索
【公告】阿斯蘭侃吧啟用https訪問
【公告】从今天开始，本站实行主题编号制
【新功能】图片缩放功能上线了