Lean 学习笔记——1. 语言概述与思维转换
Some content in this article was created with AI assistance. Please verify as needed.如果只看 def、函数调用和模式匹配，Lean 很像一门语法稍显特殊的函数式语言。实际写起来，类型检查会计算表达式，递归函数可能要证明终止，tactic 生成的定理还要再交给 kernel 检查。普通语言的编译流程不足以解释这些现象。 Lean 用依赖类型统一描述程序与证明。语法本身不算难记，先要放下“类型只约束运行时数据”这一习惯。本篇整理后续内容所需的语言背景。 语言定位编程语言与定理证明器Lean 是基于依赖类型理论的交互式定理证明器，也是一门严格求值的纯函数式语言。普通函数、数学定义、证明以及编译期扩展都写在 Lean 中，并登记到同一个声明环境。区别在于声明的类型以及代码在哪个阶段执行。 作为编程语言，Lean 有代数数据类型、模式匹配、高阶函数、类型类、Monad、宏和原生代码编译器。它的表面结构与 Haskell、OCaml 有不少相似之处。作为定理证明器，Lean 把命题放在 Prop 中，把证明...
一道高考压轴数学题的 Lean 形式化证明
Some content in this article was created with AI assistance. Please verify as needed.数学题目 问题（2008 年江西） 已知函数 $$ f(x) = \frac{1}{\sqrt{1+x}} + \frac{1}{\sqrt{1+a}} + \sqrt{\frac{ax}{ax+8}}, \qquad x\in(0,+\infty). $$ 求证：对任意正数 $a$，始终有 $1<f(x)<2$. 原问题可以自然转换为如下的三元不等式： 对任意满足 $u,v,w>0$, $uvw=8$ 的实数 $u,v,w$，证明 $$ 1 < \frac1{\sqrt{1+u}} + \frac1{\sqrt{1+v}} + \frac1{\sqrt{1+w}} < 2. $$ 自然语言证明下面用自然语言给出这道题的证明。 从证明的角度来说，下面的推导会显得非常啰嗦，但是这里的目的是为了与 Lean 代码中的四个引理/定理的证明内容保持对应。 ...
LaTeX 编译引擎跨平台基准测试
这里是一份 LaTeX 引擎跨平台基准测试脚本，用于对比各个编译引擎的编译耗时以及增量编译效率，并生成一份测试报告。 测试报告示例 测试内容 纯英文：比较 pdfLaTeX、XeLaTeX、LuaLaTeX； 中文：比较 XeLaTeX、LuaLaTeX，不测试 pdfLaTeX； 从空辅助目录开始的完整编译； 修改少量源码并保留 .aux、.toc 后的增量编译； 自动输出包含逐轮测量、汇总统计和环境元数据的 JSON，以及编译日志和测试 PDF； 自动生成一页式中文性能简报，重点比较相同工作负载下不同引擎的速度、排名和相对差距； 图表包含 P50、样本区间误差线，并将冷启动到增量构建的加速比作为附带指标； 测试结束后在控制台直接输出各文档、各构建模式下的引擎排名和主要结论。 脚本只使用 Python 标准库。测试机器需要安装 Python 3.8 或更高版本以及 TeX Live，并确保 latexmk、pdflatex、xelatex、lualatex 位于 PATH。TeX Live 还应包含 ctex、Fandol 字体、pgfplots、booktabs、...
Minecraft Java 版笔记
Some content in this article was created with AI assistance. Please verify as needed.Minecraft Java 版的模组生态围绕启动器、加载器、模组、光影、存档几个核心概念展开，本文按从底层到上层的顺序逐一整理。 启动器与实例启动器是管理 Minecraft 实例的工具，负责下载游戏本体、管理模组加载器和构造启动命令。常见的有 PCL2、HMCL、Prism Launcher 等。 启动器最终会构造一条 Java 命令来启动游戏： 123456java \ -Xmx8G \ -Djava.library.path=/path/to/natives \ -cp "minecraft.jar:loader.jar:lib-a.jar:lib-b.jar" \ net.minecraft.client.main.Main \ --gameDir /path/to/instance 实例是一套相对独立的运行环境，不同实例可以使用不同的 Minecraft 版本、加载器、...
Lean 安装与环境配置
Some content in this article was created with AI assistance. Please verify as needed.Lean 是一个函数式编程语言和定理证明器，它的版本管理和环境配置可以分成两部分来看： elan：负责 Lean 版本管理 lake：负责 Lean 项目构建和包管理 这套工具链的设计和 Rust 的 rustup + cargo 以及 Julia 的 juliaup + Pkg 非常相似，可以说是现代编程语言工具链的标配方案。 Lean 官网的 安装教程 为什么那么喜欢把 Lean 的安装和微软自家的 VSCode 生态绑定？ 虽然 VSCode 的 Lean 插件提供的辅助操作很方便，但是显然 手动安装 才是 best practice，用户能知道这里到底发生了什么，即使是基于 Lean 插件的安装教程也不过是把 Lean 的安装放在了 VSCode 中执行。 除了官网教程，还可以参考 Lean Prover 中文文档。 Lean 工具链介绍Lean 官方工具链（toolchain）包含程序开发所需...
Rust 安装与环境配置
Rust 是目前最著名的 C++ 替代语言，它的版本管理和项目管理由两个组件提供： rustup：Rust 工具链版本管理 cargo：项目构建和包管理 对比 C++ 生态：rustup 管理编译器版本（C++ 没有标准的编译器版本管理器），cargo 融合了 CMake（构建）、vcpkg/Conan（包管理）和 CTest（测试）的功能。Rust 的标准工具链解决了 C++ 生态中长期以来需要拼凑不同工具才能覆盖的问题。 下面主要关注 Linux 环境下的使用，macOS 高度类似；Windows 中路径不同但概念一致。 Rust 工具链目录rustup 管理的安装目录： 123456789101112131415~/.rustup/├── settings.toml├── update-hashes/└── toolchains/ -- 各个版本的 Rust 工具链 ├── stable-x86_64-unknown-linux-gnu/ │ ├── bin/ │ │ ├── rustc ...
LLM 学习笔记——模型与 Agent 基础知识
Some content in this article was created with AI assistance. Please verify as needed.本文关注大模型的用户使用，整理一下大模型与 Agent 工具的基础知识。 大模型分类大模型可以按定位分类： 旗舰模型 日常模型 低成本模型 多模态模型 … 还可以按开放程度可以分类： 闭源模型：只能通过官方产品、API、云平台或聚合平台访问。通常能力领先、产品体验完整，但版本和价格由厂商控制。 开放权重模型：公开权重和主要架构信息，但训练数据、训练代码和完整训练流程通常不公开。优点是可私有部署、可固定版本、可微调。 完全开源模型：尽量公开训练代码、数据处理、权重和复现流程，多见于研究社区。 常见概念 上下文窗口：指模型一次调用能看到的 token 总量，包括输入、历史对话、工具结果、文件内容和系统提示等 由于长对话每次会把之前所有对话内容都提交，在内容长度接近上下文窗口时，需要使用 Agent 工具对之前的对话内容进行压缩（手动压缩或自动触发） 越强的大模型，支持的上下文窗口越大。但是实际使用中，长对话的...
纯 Python 实现深度学习代码
microgpt.py 是 Andrej Karpathy 写的一个教学项目，几百行纯 Python 实现完整的 GPT 训练和推理流程，不依赖 PyTorch，甚至不依赖 Numpy！ 受到这个项目的启发，我们在原有代码的基础上进一步扩展，从标量自动求导框架开始，依次实现 MLP、RNN、LSTM 和 Transformer 模型，仍然保持纯 Python 的风格，当然代价就是比基于 PyTorch 等的实现慢很多。由于这里只是作为演示项目，训练得到的模型看起来还是在胡言乱语。 自动求导由于不依赖 PyTorch 和 Numpy，首先需要一个 Value 类来实现自动求导，为后续的训练和推理提供基础。 训练神经网络的核心是知道损失函数 $L$ 对每个参数 $\theta$ 的梯度 $\partial L/\partial\theta$，再沿梯度反方向更新参数。手工推导每一层的梯度既繁琐又容易出错，自动求导则把前向计算记录成一张计算图，然后从损失节点开始反向应用链式法则。 例如 $y=f(g(x))$，链式法则为 $$ \frac{\partial y}{\p...
LLM 代码练习——使用大模型绘图
从 K-Dense-AI/scientific-agent-skills 的科技论文绘图 skill 中抄来的绘图提示词。 调用源码 12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717...
矩阵链乘法问题
问题描述在科学计算中，我们经常需要计算多个矩阵的乘积。由于矩阵乘法满足结合律，而各个矩阵的规模可能差异很大，通过改变乘法的计算顺序（即添加括号），对实际的计算量会有显著的影响。 对于矩阵 $A \in \mathbb{R}^{r \times s}, B \in \mathbb{R}^{s \times t}$，计算乘积 $A B \in \mathbb{R}^{r \times t}$ 的每一项都需要 $s$ 次乘法，因此乘法计算量为 $r s t$。 例如计算 $A B C$，A 的尺寸为 500×2，B 的尺寸为 2×500，C 的尺寸为 500×2，下面两种运算顺序的乘法运算量有巨大差异： $(A B) C$ 的运算量为 $O(500\times 2 \times 500) + O(500 \times 500 \times 2)$； $A (B C)$ 的运算量为 $O(2\times 500 \times 2) + O(500 \times 2 \times 2)$。 我们希望使用最优的一种做法来加速计算，这就是矩阵链乘法（Matrix-chain multipl...