- 收录文章
- 19 篇文字被发现
- 文章访问
- 12 次从这里出发阅读
- 博客访问
- 1 次前往作者站点
- 最近更新
- 05.13 2026年
FROM THIS BLOG
最近文章
后缀自动机是怎么被构造的？它的复杂度又是如何证明的？
本文尝试以一种较为直观的角度看待后缀自动机、后缀链接树和结束位置集合，并尝试给出关于状态数、转移数和时间复杂度的证明。
W4terCTF 2026 出题记录和题解
本文包含了 W4terCTF 2026 中我出的三道题目以及对应的题解，分别为“优质 Flag 募集中”，“日历・序章”和“日历”。
使用 Typst 完成 Advent of Code 2023 之后，我学到了什么？
本文是我在使用 Typst 完成 Advent of Code 2023 之后的一些心得和体会。在这篇文章中，我将分析 Typst 在编写算法竞赛题目方面的局限性，并分享一些有趣的实现细节。
Natural Number Game 第九部分 / 高级乘法世界
本文介绍了 Natural Number Game 中的第九部分，主要涉及一些更复杂的乘法定理，例如乘法消去律等。
Natural Number Game 第八部分 / ≤ 世界
本文介绍了 Natural Number Game 中的第八部分，主要涉及自然数上的不等关系 ≤ 的一些基本定理，例如反身律、传递律、全序等。
Natural Number Game 第七部分 / 高级加法世界
本文介绍了 Natural Number Game 中的第七部分，主要涉及一些更复杂的加法定理，例如消去律等。
Natural Number Game 第六部分 / 算法世界
本文是 Natural Number Game 的第六部分，主要介绍了 Lean 中的算法相关定理的证明，包括和式整理、前驱数、自然数的比较等定理。
Natural Number Game 第五部分 / 幂世界
本文是 Natural Number Game 的第五部分，主要介绍了 Lean 中的指数相关定理的证明，包括零的零次幂、任何数的一次幂、乘积的幂次等定理。
Natural Number Game 第四部分 / 蕴含世界
本文是 Natural Number Game 的第四部分，主要介绍了 Lean 中的蕴含逻辑相关定理的证明，包括 exact 和 apply 策略的使用，以及如何在 Lean 中处理蕴含关系等定理。
Natural Number Game 第三部分 / 乘法世界
本文是 Natural Number Game 的第三部分，主要介绍了 Lean 中的乘法相关定理的证明，包括乘法的交换律、结合律，以及乘法对于加法满足的分配律等定理。
Natural Number Game 第二部分 / 加法世界
本文是 Natural Number Game 的第二部分，主要介绍了 Lean 中的归纳法证明策略，并通过一系列关卡证明了加法的交换律与结合律等定理。
Natural Number Game 第一部分 / 教程世界
本文是 Natural Number Game 的第一部分，主要介绍了 Lean 中的基本证明策略，包括 rfl 和 rw 等，并在最终证明了 2 + 2 = 4。