首頁
>
lean4吧
>
瀏覽帖子
中文（台灣正體）
英語
中文（大陆简体）
中文（港澳繁體）
中文（马新简体）
|
登錄
|
註冊
進入侃吧
進入個人空間
全部
僅作者
目前共有
2
篇帖子。
字體大小：
較小 - 100% （默認）
▼
內容轉換：
不轉換
▼
點擊
回復
175
1
荒废了很久，重新开始学习，现在AI也能写lean4了
悄悄打开魔盒
大魔導士 十七級
回復
1樓
發表於：
2026-4-20 00:43
25000行代码的素数定理证明，20万行代码的球堆积问题证明，规模越来越大
悄悄打开魔盒
大魔導士 十七級
回復
2樓
發表於：
2026-4-20 00:52
上次到第五章以后就没再继续，这次争取学完MIL全篇，有时间再看TPIL
回覆帖子
內容：
圖片
視頻
表情
用戶名：
您目前是匿名發表。
驗證碼：
看不清？換一張
（快捷鍵：Ctrl+Enter）
本帖信息
點擊數：
175
回複數：
1
作者：
悄悄打开魔盒
最後回覆：
悄悄打开魔盒
最後回復時間：2026-4-20 00:52
公告板
【新功能】现在手机版发帖也可以上传图片了
【公告】布拉斯侃吧（Purasbar）全站已启用HTTP/2访问以及TLS1.3加密
【新功能】楼中楼功能已上线
【公告】Purasbar http访问方式已关闭，从现在起只能通过https方式访问
【新功能】现在可以直接在发帖框中粘贴图片啦！
【新功能】搜索框提示功能上線了
【公告】第十五次補丁包安裝完畢
【公告】從現在開始，管理員將停止審批會員
【公告】阿斯兰侃吧现在开始支持简繁混合搜索
【公告】阿斯蘭侃吧啟用https訪問
【公告】从今天开始，本站实行主题编号制
【新功能】图片缩放功能上线了
