高中几何coq
https://github.com/coq-community/HighSchoolGeometry
用lean4刷一下历届奥数题熟悉tactic也是个不错的选择，思维体操:cartwheel:。
Title: Formalization of IMO shortlist problems in Lean 4
一键打开：https://gitpod.io/new/#/https://github.com/chenjulang/IMOSLLean4
链接：https://github.com/mortarsanjaya/IMOSLLean4
对应文字证明搜索网站：.tex文件里面有写。
没有的话在这里搜：https://artofproblemsolving.com/wiki/index.php?search=2006+Consider+the+sequence&title=Special%3ASearch&profile=default&fulltext=1
说到这个，lean组织重要成员Floris van Doorn发的这个14课教程也推荐大家看，第6课讲到classical.choose
链接：https://github.com/fpvandoorn/LeanCourse23
用lean解决99个小问题，从逻辑到算法到数据结构陆续都有的：
链接：https://github.com/lean-ja/lean99/tree/main
c5739f378dcc0db884cf52601c0eb577.png
哥德尔第一不完备性定理，链接：https://github.com/iehality/lean4-logic/blob/master/Logic/FirstOrder/Incompleteness/FirstIncompleteness.lean
《数学天书中的证明》https://github.com/mo271/formal_book，看到这个第一章就用6种方法证明素数无限[表情]
链接：https://github.com/m4lvin/lean4-pdl
这个项目应该是从零构建了精益 4 中的命题动态逻辑
5c4afe853d9c12849d80b380b4e087af.png
离散傅立叶变换等的相关证明
链接：https://github.com/YaelDillies/LeanAPAP/blob/71f7ae79decdf1cb2acd818fdbcc2db1ea3d81f1/LeanAPAP/Prereqs/Discrete/DFT/Basic.lean#L8
一个通过自然语言写出命题的Lean4库
链接：https://github.com/siddhartha-gadgil/LeanAide
一个炫耀元编程水平(400行代码)的走迷宫游戏，证明完也是走出迷宫的过程。
在线体验：https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fdwrensha%2Flean4-maze%2Fmain%2FMaze.lean
链接：https://github.com/dwrensha/lean4-maze?tab=readme-ov-file
1aa9da597d9b6b37ded1edadb2ce21df.png
当然安利一下我的魔方证明项目哈～～
https://github.com/chenjulang/rubikcubegroup
https://github.com/chenjulang/rubik_cube
链接：https://github.com/leanprover-community/ProofWidgets4
6d9eb878b597478b19664060f4221c3f.png
lean4实现Lambda 演算Lambda Calculus
链接：https://github.com/edusporto/lambda-lean/tree/main
Kevin Buzzard的针对本科数学生的lean4教程
链接：https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/Introduction/introduction.html
Tactic documentation：
https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/Part_C/tactics/tactics.html#
原来也有人在整理lean4的资料，点赞
链接：https://github.com/34j/best-of-lean4
这个视频挺有趣的，程序员+哲学家与数学家2人同时学习lean4，不失为一个好方法。
链接：https://www.youtube.com/watch?v=FPiykrdPe6U&list=PLCTMeyjMKRkoGpN4-7mRbABd02P1xy6gh&index=1
一切皆可漫：
链接：https://www.nicovideo.jp/tag/Lean
46d6df2b81051df2d971607900ce43fa.png
然后这个是难度大一点的硕士生Lean4教程：
链接：https://github.com/adomani/MA4N1_2023
陶哲轩从零学习Lean4过程记录23年10月10日开始：
链接：https://mathstodon.xyz/@tao
他用GPT4玩自然数游戏的全记录：https://chat.openai.com/share/857353ad-a05b-4f9e-bb10-55f15a2bd871
后面就不一一赘述了
大模型配合LEAN, on your laptop or in the cloud：LLMs+Lean
链接：https://github.com/cmu-l3/llmlean
3c1164e711f03e4101e2edde35f5ba8a.png
思维体操系列，一些数学难题的lean4证明
链接：https://github.com/dwrensha/compfiles/tree/main/Compfiles
《骑士与无赖》逻辑谜题的相关证明
链接：https://github.com/tydeu/folktale
纽结理论思想的一些形式化
链接：https://github.com/shua/leanknot/tree/lean4
继之前的证明MergeSort算法的合理性以后，这里还有一个证明时间复杂度的。
lean3链接：https://github.com/tomaz1502/RunTimeFormalization
lean4版本: https://github.com/tomaz1502/RuntimeFormalization4
分享一个一键打开旧Lean3项目的方法，非常简单，以这个《数学女孩》项目为例子：
链接：https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Open.20any.20Lean3.20project.2E
AI for Math
1a2ee161db9e160b83e259a3b2fc351a.png
链接：https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0/edit
一个群友的工作
链接：https://gitee.com/hoxide/zerosum
这是王浩成。我代表我们课题组介绍一下我们厦门大学马来西亚分校数学系的LEAN课题组。我们组包括三名自2023年8月开始从事数学形式化和证明工作的本科生，以及我们的导师马家俊博士。在不到一年的时间里，我们已经解决了博弈论形式化的主要部分，并取得了一些成就。拍卖理论：包括第一价格拍卖中的非主导策略、DSIC（主导策略激励兼容）机制以及第二价格拍卖中的非负效用的形式化证明。迈尔森引理：最优拍卖为卖家解决了广泛的拍卖设计问题。拓扑标准单纯形是紧致的
链接：https://github.com/ImperialCollegeLondon/complex-number-game
The Complex Number Game 复数游戏
链接：https://github.com/ImperialCollegeLondon/formalising-mathematics-2024/tree/main/FormalisingMathematics2024/Section21galoisTheory
Kevin的另一个入门课程，21课时从逻辑一直讲到伽罗瓦理论
Lean4 中幺半群类别中图解推理的图形重写
链接：https://github.com/dignissimus/Untangle
2f02ea0ec1c01246edbcf2b60dd0a33e.png
该脚本可以检查并自动生成lean4存储库中的“导入”语句。
链接：https://github.com/Seasawher/import-all?tab=readme-ov-file
图形着色相关的证明
链接：https://github.com/kmill/lean-graphcoloring/tree/master
主要讲元程序还介绍了这个走迷宫游戏。
链接：https://www.youtube.com/watch?v=n1Pd0GeHsAY
knots + 2D展示 + 定理证明 + 图形操作绑定LEAN定理命题
这个也是很不错的数学科普项目，让小学生也能凭借直觉折腾出一些“数学定理”
纽结理论思想的一些形式化
链接：https://github.com/shua/leanknot/tree/lean4
7e64d93af20cfc7c520c727a221bf6c5.png
通过在 Agda 中实现《编程语言基础》这本书中的证明来学习 Lean 4 的旅程
链接：https://github.com/rami3l/plfl
robo游戏更新了，function级别有新增27关，有空快来玩[表情]
链接：https://adam.math.hhu.de/#/g/hhu-adam/robo
e99c4457a235343472f258f0c2eeb213.png
有空更新Mathlib以免有的定理用不了，更新Mathlib的方法之一： curl -L -O https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain lake update lake exe cache get
chenjulang: 给数学家角度上的LEAN课，9个方向的大佬手把手教学LEAN基础一直到代数几何，微分几何等等～～～，虽然2023年但是也不显得过时： 视频链接：https://www.youtube.com/watch?v=Ft_3jDl3qxQ&list=PLlF-CfQhukNn7xEbfL38eLgkveyk9_myQ&index=1 仓库：https://github.com/lftcm2023/lftcm2023/blob/master/README.md 还有2024年的： 仓库：https://github.com/riccardobrasca/LFTCM2024/blob/master/README.md 暂时找不到视频资源，但是文件的注释已经在讲解了，挺好理解的。
chenjulang: 线性代数学习游戏，链接：https://stavan-jain.github.io/linear_algebra_game/
仓库：https://github.com/Stavan-Jain/linear_algebra_game
另一个lean4版本的：https://github.com/hhu-adam/LAG
chenjulang: 各个数学分支的形式化学习2022，链接：https://github.com/ImperialCollegeLondon/formalising-mathematics-2022
应该是有视频的：https://www.youtube.com/watch?v=3XaL0tjnWSk&list=PLVZep5wTamMmRPvCLO4WVpCwkTi1F6OyF。
每年难度是逐步增加的，所以最好从年份早的开始看，2021：https://github.com/ImperialCollegeLondon/formalising-mathematics
chenjulang: 帝国理工的教学资源。只会嫌多，不会嫌少，链接：https://github.com/orgs/ImperialCollegeLondon/repositories?q=lean
chenjulang: 分享一个一键打开旧Lean3项目的方法，非常简单，以这个《数学女孩》项目为例子：
链接：https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Open.20any.20Lean3.20project.2E
一句话就是按照这个项目：https://github.com/chenjulang/lean-mathgirls
将两个文件加进去，提交到github，然后添加前缀
Dockerfile
.gitpod.yml
https://gitpod.io/new/#/
打开后不要急，报错不用管，右下角有一个leanpkg什么的点击一下，然后等待目录里面有一个_target下载完Mathlib就可以用了。
chenjulang: 内存不足运行：leanproject get-mathlib-cache
chenjulang: Mathlib import失败要切换leanpkg.toml的rev
又收集了很多无聊可以玩着学LEAN的游戏： 1.度量空间与拓扑游戏：https://github.com/lnay/metric-spaces-and-topology-game/tree/main 2.希尔伯特公理学和公理几何游戏：https://github.com/mmasdeu/argo/blob/main/README.md 3.Filter游戏：https://github.com/Biiiilly/filter 4.数独游戏：https://github.com/TwoFX/sudoku 5.群论游戏：https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/orbit/basic.lean 6.猜数字游戏：https://github.com/foxthomson/guessgame
又收集了很多无聊可以玩着学LEAN的游戏：
1.度量空间与拓扑游戏
2.希尔伯特公理学和公理几何游戏
3.Filter游戏
4.数独游戏
5.群论游戏
6.猜数字游戏
Programming with Math | The Lambda Calculus
视频链接
https://www.youtube.com/watch?v=ViPNHMSUcog
LEAN 4 中的凸优化建模，github
https://github.com/verified-optimization/CvxLean/raw/main/CvxLean/Demos/README.gif
chenjulang: Agda的数学库
chenjulang: 使用立方体理论将经典数学形式化
已经正式化的事情的一瞥：
Results concerning classical axioms, especially Diaconescu's theorem;
关于经典公理的结果，特别是迪亚科内斯库定理;
Classical impredicative powerset, setting up a structural set theory;
经典的不定幂集，建立结构集合论;
Topological spaces, compactness, Hausdorff axiom and metric spaces;
拓扑空间、紧致性、豪斯多夫公理和度量空间;
Construction of classical Dedekind real, and it is a complete Archimedean ordered field;
构造经典的戴德金实数，它是一个完整的阿基米德有序场;
Basic theorems of real number including monotone convergence theorem, Heine-Borel theorem, Bolzano-Weierstrass theorem and the convergence of Cauchy sequences;
实数基本定理，包括单调收敛定理、海涅-博雷尔定理、玻尔扎诺-魏尔斯特拉斯定理和柯西序列收敛;
Intermediate value theorem of continuous real functions.
连续实函数的中值定理。
chenjulang: 中文作者函数式程序语言简介
Functional Programming 知識大補帖
chenjulang: Coq/SSReflect 中的交换代数
chenjulang: 在 Agda 的 HoTT 书中形式化证明
chenjulang: Introduction_To_algorithms (Coq)
chenjulang: 类似 CoqIDE 的 kakoune 体验
示意图
chenjulang: Agda在线版
chenjulang: Agda的数学库
Yifan Song(义和团二当家): Tactic 相关
全tactic:
import Mathlib.Tactic
All tactics generated from #help tactic
Lean tactic cheatsheet with examples in 日语
沉浸式翻译插件
immersed translation
chenjulang: 说到翻译软件顺便安利一个TTime，可以截图翻译,deepl等多种专业翻译，无限额度，专门对付一些老的纯图片的PDF。
Yifan Song(义和团二当家): Linux 用户表示你在说什么
chenjulang: Hacking Lean in Lean Book 链接
chenjulang: awesome coq
chenjulang: The Lean Mathematical Library 本文介绍了 mathlib，这是一项由社区推动的计划，旨在构建一个统一的数学库，该库在精益证明助手中形式化。在证明助手库中，它的特点是依赖类型的基础、专注于古典数学、广泛的结构层次结构、大规模和小规模自动化的使用以及分布式组织。我们解释了该库的架构和设计决策以及导致其发展的社会组织 链接
目录： 摘要 >1简介 2 Lean 3mathlib 的内容 >4类型类 >5线性代数 >6元编程 >7社区 >8与其他库的比较 9结论 致谢 参考文献
chenjulang: The Type Theory of Lean 链接
目录(机翻)： 目录 简介 1.1 编程语言中的类型理论 1.2 类型理论的集合论模型 2 公理 2.1 类型化。 2.2 定义相等 2.3 归约。 2.4 let 绑定器（（归约） 2.5 定义（归纳） 2.6 归纳类型.. 2.6.1 归纳规范 2.6.2 大消除 2.6.3 递归器 2.6.4 计算规则（归纳） 2.7 非原始公理 2.7.1 商类型 2.7.2 命题外延性 2.7.3 选择公理 2.8 与 Coq 的区别 3类型系统的属性 3.1定义相等性的不可判定性 3.1.1算法相等性不是传递性的 3.1.2主题归约失败.. 3.2规律性.. 唯一类型 4 4.1k归约 4.2Church-Rosser定理 归纳类型归约到W类型 5.1动物园 5.2转换类型家族。 5.3转换子单例消除器 5.4余数 6健全性 6.1证明分裂 6.2 2ZFC中的精益建模。 6.2.1 ZFC中W类型的定义 6.2.2 ZFC中acc的定义。 6.3健全性.. 6.4类型注入...
chenjulang: Lean程序验证的新手教程： 链接
目录： |基础 >1类型和术语 >2程序和定理 >3向后证明 >4向前证明 Il函数逻辑 编程 >5函数编程 >6归纳谓词 >7有效编程 >8元编程 l程序语义 >9操作语义 >10霍尔逻辑 >11指称语义 IV数学 >12数学的逻辑基础 >13基本数学结构 >14有理数和实数 参考书目
chenjulang: Eudoxus Reals提供了一种严格的方法来定义实数，并证明了它们的基本性质，比如实数的稠密性、有序性等。 仓库
chenjulang: 《The Little Typer》是一本面向那些没有正式学习过逻辑或编程语言理论，但想要理解依赖类型理论核心思想的程序员的书。虽然上述所有资源的目标都是尽可能实用，但the Little typer提供了一种实现依赖类型理论的方法，在这种方法中，最基本的东西都是从头开始构建的，只使用编程中的概念。《精益函数式编程》的作者同时也是《The Little Typer》的作者。 链接
de3c646df8428bb54a5d2aba3c36fde2.jpeg
chenjulang: 《 软件基础》（Coq）和《 编程语言基础：Agda 描述》的翻译
chenjulang: @Oling Cat·欧林猫 这个学习教程就有点意思了，交叉了这位群友的翻译工作。 通过实施 Agda 的精彩书籍 Programming Language Foundations 中的证明来学习精益 4 的旅程。 链接
chenjulang: 1.附有在线版练习的Coq系统教程。该库还构成了四色定理和奇数阶定理的机器检查证明的基础结构。 链接
2.精益求精的数学家 2024 仓库 视频链接 有翻译的视频在这里
chenjulang: Lean验证菲尔兹奖得主Peter Scholze关于凝聚态数学的一系列定理，截至 2022 年 7 月 14 日星期四 15：46：13（美国东部标准时间），液体张量实验已经完成。 介绍 仓库
d12b6cd3127f6ce033093123df0da1c8.jpeg
chenjulang: 费马大定理的机器形式化证明蓝图。也可以导入自己的项目看看
55f2648c9043d27b949f1d9a47cff212.jpeg
chenjulang: Mathlib explorer 是专为 Lean 的 mathlib 库设计的交互式可视化工具
Scroll to zoom in/out 滚动放大/缩小 Drag to move 拖动移动 Click on a node to highlight 单击要突出显示的节点 its direct neighbors 它的直接邻居 its transitive dependents 其及物从属 its transitive dependencies 其传递依赖关系 Click on a topic label to highlight 单击主题标签以突出显示 all nodes in the same topic 同一主题中的所有节点 references to the topic 对主题的引用 direct dependencies of the topic 主题的直接依赖关系
https://gdynamic.qpic.cn/gdynamic/BNUEGVfXeY3wyAYQibib7K9QicuDQQzIibElJGBWScDqeQk/628
33e486ab5ff30efffcfab0d79ec470cd.jpeg
chenjulang: 《102 Combinatorial Problems》一书中（一些）问题的证明 链接
chenjulang: 很多LEAN的内容都是直接移植Isabelle的，所以很有必要会用。 浙大在线版 支持多个版本并行～～
5e2d29137f855a091f74babb3393c876.png
chenjulang: Lean可以参考Coq很多证明过的案例，Coq的项目很多都是从零构建定义和符号的，，通过渐进式的过程很适合初学者领悟形式化的思想，在线测试Coq代码： 以这个分析基础为例：
Coq的在线版本：https://coq.vercel.app/ 创建新的代码编辑器，然后直接将代码粘贴进去就可以用了。点击右上角的向下箭头实时编译查看证明步骤。
1b5b31c74d3c98fd69902d6cf3b49050.png
chenjulang: 1.Tao写的 Newton inequalities。链接
2.该存储库包含一个简单的精益项目，可以在 GitHub CodeSpaces 上一键启动该项目。 链接
3.一个理学学士最终项目：使用精益形式化排序算法的运行时间复杂度。 链接
chenjulang: Mathlib4的所有tactics，对，全部都有。包括定义的位置，基本解释，用例。 链接
chenjulang: LEAN语法速查（右上角一键在线例子）： 链接
LEAN命令+策略速查（右上角一键在线例子）： 链接
a107d89bc81a09ff9cde3c6455e5e906.png
通过代码示例学习精益语言https://github.com/lean-ja/lean-by-example
chenjulang: 高斯积分的证明
221482945ddd0a3b1ab4412737595d9f.png
chenjulang: 从Mathlib4按需拆出子项目的示例，零依赖Mathlib4
chenjulang: 1.[实数理论])https://github.com/ImperialCollegeLondon/real-number-game )
2.求解丢番图方程
3.针对本科数学家的精益项目的一些示例
4.About Condensed mathematics
5.Dots and Boxes游戏
chenjulang: 零依赖的詹森不等式证明： 链接
chenjulang: show_term的强大作用之一：解开任意tactic成最小步骤。 例如这里将ring的实际源码级别的分步操作打印出来了。
https://gdynamic.qpic.cn/gdynamic/BNUEGVfXeY0IiaVicpv0SELGm9nfX0mZ3NI7g9U0dgU4E/628
chenjulang: Kevin教授做的一个独立于Mathlib4的从零构造学习骨架 链接
chenjulang: china software 2024形式化论坛直播回放
chenjulang: 大家可以从自己感兴趣的领域回溯到起点，不失为一种学习源码的方法。 具体方法：
1.github打开你感兴趣的文件。
2.点击时间回溯“Commit history”。
3.找到最早的提交记录（如果它注释是从别的仓库复制来的，就要去到该旧仓库找回该时间点前的文件）。
4.进入任何提交后，都可以点击“Browse file”得到一个该时间点的项目切片，这个非常好用哦。 比如从这里群论基础文件，从零看起非常的有趣，
chenjulang: 不同的排序证明思路：插入排序+选择排序的合理性证明。 链接
chenjulang: 范畴论游戏： 链接
另外还有一个范畴论形式化项目： 链接
chenjulang: 顺便总结一下如何更新lean版本到最新哈： 首先是执行图中的两个命令。然后将自己项目的lean-toolchain文件里面的版本号，也就是v后面的版本改成上述命令执行完后显示的那个最新版本即可。
https://gdynamic.qpic.cn/gdynamic/BNUEGVfXeY12qFrWwD9AFLs8jrtZRoCZ9DjO71BUhico/628
chenjulang: Coq也有一个游戏：推箱子游戏，还有20关～～～骚操作 链接
chenjulang: 范畴论（Type theory）杂谈很适合找到你的兴趣点。链接【合集·Cat Talks 范畴论系列课程-哔哩哔哩】
chenjulang: 归并排序算法的lean数学证明fecssk-solutions
交互式定理证明与程序开发Coq归纳构造演算的艺术-by-顾明.pdf
chenjulang: coq分析基础
chenjulang: 群友@Qiu写的归并排序
入职字节LEAN实习的群友@Qiu写的冒泡排序
很久以前的吴方法在Isabelle的形式化，文章里介绍了太多的几何自动证明等相关的网址，这里就不一一赘述了，赶紧戳进去看看。
自动几何推理论坛ADG 2023
多种几何自动验证软件下载。
Geometry 几何学
Poincare disc model of hyperbolic geometry 双曲几何的庞加莱圆盘模型
Complex geometry 复杂几何形状
Tarski's book 塔斯基的书
Automated verification of high school geometry 高中几何图形的自动验证
Automated verification of informal proofs 非正式证明的自动验证
image.png
chenjulang: 专门做几何形式化和自动证明的教授，他的首页包括很多coq和isabelle的各种射影几何、塔斯基公理系统等琳琅满目的证明和软件。link
chenjulang: 还有俩1，2
chenjulang: 几何证明其中一个在线预览一下：gclc，可以用吴方法等
今年3月才开始有web版，软件发布30年有上万用户了，快去自动证明一下吧～～
：
1.在线版
2.介绍首页
3.使用手册
image.png
image.png
image.png
举例：
95ff9ed567f70e37ce1ffae33d36a1b5.png
简单证明这两个三角形面积相等。
area方法证明.pdf
wu.pdf
chenjulang: [Tactics & Keyframes: Visualizing Lean 4 Proofs in Blender]
(https://www.youtube.com/watch?v=KuxFWwwlEtc)
有一个国际象棋游戏在里面
lean证明动画演示.mkv
chenjulang: Catalog Of Math Problems Formalized In Lean
https://xenaproject.wordpress.com/
Xena项目是由数学家Kevin Buzzard在伦敦帝国学院领导的一项倡议，旨在通过将计算机证明系统（如Lean）融入本科课程，培养擅长使用交互式策略进行数学研究和探索的新一代数学家，从而改变数学教育方式。
chenjulang
10:19 PM
Karpathy llm.c in Lean 4 (because lean ffi is too obscure)
link
https://www.youtube.com/watch?v=W0w5JCod5sE
chenjulang: 强烈推荐：Lean每日一题。链接
image.png
chenjulang: 一个youtuber持续更新，小白Lean入门， LeanFirstSteps
Yifan Song(义和团二当家): 他这个realtion and partition 的定义太奇怪了
chenjulang: 对啊
chenjulang: 形式化高斯消元算法
chenjulang: Formal Verification of Coalescing Graph-Coloring Register Allocation
chenjulang: Dijkstra 的算法，用于查找 a 和 b 之间的最短路径。目前貌似只在Isabelle形式化了，一个很好的学习切入点。
chenjulang: 给你整理送饭视频，教授的科普视频：
【The Future of Mathematics?-哔哩哔哩】 https://b23.tv/wgV5TzJ
【【英字】The Future of Mathematics？IMO满分得主、代数数论专家力推定理证明器-哔哩哔哩】 https://b23.tv/bw8Ipsy
【凯文 · 巴扎德 ：数学和计算机 G-Research-哔哩哔哩】 https://b23.tv/rQXVhoT
【What Computers Can't Do - with Kevin Buzzard-哔哩哔哩】 https://b23.tv/o7poqS5
【Kevin Buzzard - 计算机会证明定理吗？-哔哩哔哩】 https://b23.tv/OdO28NC
chenjulang: 我觉得国内最好的北大的Lean数学系统学习的视频，讲的非常的透彻【lalala的王子的个人空间-哔哩哔哩】 https://b23.tv/FJYsb8V
chenjulang: C++尝试做了一个类似的数学命题证明demo。【【整活】C++居然可以证明数学命题！-哔哩哔哩】 https://b23.tv/HH8DGmT
chenjulang: coqpilot,配合coq分析基础来食用更好哦
https://github.com/JetBrains-Research/coqpilot/blob/main/etc/gif/solve-in-selection.gif
chenjulang: The leanest proof of Zorn's Lemma 佐恩引理
manuscript
formalized it
Zorn 引理是说, 如果一个偏序集的每个全序子集都有上界, 那么这个偏序集就有极大元.
Zorn 引理常常用来说明极大对象的存在性.
例如, 向量空间的基是极大的线性无关子集, Zorn 引理可以说明每个向量空间都有基. 再例如, Zorn 引理可以用来证明 Krull 定理: 一个环的任何真理想都包含于一个极大理想.
在 ZF 集合论中, Zorn 引理与选择公理等价. 因此, 在主流数学所使用的 ZFC 集合论中, Zorn 引理是真命题.
在构造主义数学中, 选择公理蕴涵 Zorn 引理, 而 Zorn 引理需要加上排中律才能推出选择公理.
佐恩引理可用于证明每个连接图都有一个生成树。
sdzz gndrc: compfiles
一系列奥林匹克风格的数学问题及其解答，使用 Lean 4 形式化。
sdzz gndrc: Exploring Formalisation
A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology
Improving on AlphaProof: IMO 2024 Problem 2 in Lean 4
https://www.youtube.com/watch?v=5IARsdn78xE
Links The proof: https://gist.github.com/dwrensha/68de... Proof animation tool: https://github.com/dwrensha/animate-l... DeepMind announcement: https://deepmind.google/discover/blog...