马新简体 | 登录 | 注册
目前共有4篇帖子。 字体大小：较小 - 100% （默认）▼  内容转换：台灣正體▼
 
点击 回复
681 3
lean4教程
悄悄打开魔盒
上位魔导士 十五级
1楼 发表于：2024-5-2 16:20
回复
https://leanprover-community.github.io/mathematics_in_lean/
這個教程是關於如何用lean4和mathlib4做數學的


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

這個教程是lean4語言本身的教程，更偏向對語言機制的介紹，不包含mathlib的使用
啊啊是谁都对
副总编 二十二级
2楼 发表于：2024-5-2 17:26
回复
感覺使用lean4很像用計算機編程
 
啊啊是谁都对：有無最簡單的實例？
  2024-5-2 17:42 回复
悄悄打开魔盒：回復 @啊啊是誰都對：有的，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 回复

回复帖子

内容：
用户名： 您目前是匿名发表
验证码：
（快捷键：Ctrl+Enter）
 

本帖信息

点击数：681 回复数：3
评论数： ?
作者：悄悄打开魔盒
最后回复：悄悄打开魔盒
最后回复时间：2024-5-2 23:41

公告板

 【新功能】現在手機版發帖也可以上傳圖片了
【公告】布拉斯侃吧（Purasbar）全站已啟用HTTP/2訪問以及TLS1.3加密
【新功能】樓中樓功能已上線
【公告】Purasbar http訪問方式已關閉，從現在起只能通過https方式訪問
【新功能】現在可以直接在發帖框中粘貼圖片啦！
【新功能】搜索框提示功能上線了
【公告】第十五次補丁包安裝完畢
【公告】從現在開始，管理員將停止審批會員
【公告】阿斯蘭侃吧現在開始支持簡繁混合搜索
【公告】阿斯蘭侃吧啟用https訪問
【公告】從今天開始，本站實行主題編號制
【新功能】圖片縮放功能上線了
 
©2010-2025 Purasbar Ver2.0 ▲
除非另有声明，本站采用知识共享署名-相同方式共享 3.0 Unported许可协议进行许可。