📝 手记与博客 (Blog & Insights)
记录 SF-lean4 社区在形式化验证、现代 Lean 4 重塑实践以及程序语言理论中的探索思考与演进历程。
🌟 推荐文章
🚀 重塑经典：用现代 Lean 4 重构《软件基础》全三卷与交互式文档
日期：2026-10-18 · 作者：Ghost-Silver & SF-lean4 Community · 标签：
项目发布Lean 4软件基础形式化验证从 Coq 到 Lean 4 的 57 章全量形式化之旅。深度剖析全三卷理论框架、现代 Lean 4 惯用设计、Presburger 线性算术自动化、宏系统 DSL，以及单源真理文档工程体系的完整演化。
👉 阅读全文 →
📬 交流与探讨
如果你对博客中的话题、形式化证明策略或某些章节的 Lean 4 实现有独到见解，欢迎在 GitHub Issues 或 Discussions 中与我们交流探讨！