一道高考压轴数学题的 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 代码中的四个引理/定理的证明内容保持对应。 根式改写（引理...
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 ...
Agent 工具使用笔记——skills
Some content in this article was created with AI assistance. Please verify as needed.skills 用来给 agent 增加可复用能力。AGENTS.md 放常驻项目事实，skill 放按需执行的专业知识、流程、脚本和模板。 我理解一个 skill 至少要回答三个问题： 什么情况下使用它？ 使用时按什么步骤做？ 需要读取哪些额外参考材料、脚本或模板？ Agent Skills 的核心思想是 progressive disclosure：启动时只暴露 name 和 description；任务命中后再读完整 SKILL.md；更长的参考资料、脚本和模板等到真的需要时再加载。 适合做成 skill Hexo 新文章流程 LaTeX 编译和排错流程 发布前检查流程 code review checklist changelog 生成 数据处理报告流程 不适合做成 skill 项目简介 构建命令 禁止修改目录 API key 一次性提示词 基本结构一个 skill 是一个目录，最少包含 SKILL...
Agent 工具使用笔记——AGENTS.md
Some content in this article was created with AI assistance. Please verify as needed.AGENTS.md 是给 coding agent 看的项目说明文件，可以理解成 “README for agents”。它要解决的问题很朴素：这个仓库是什么、哪些命令可用、哪些地方能改、改完怎么验证。 它不适合写成教程，也不适合塞一堆个人偏好。越是常驻上下文，越应该短、准、稳定。 AGENTS.md 本质上就是普通 Markdown，没有固定 schema，也没有必填字段。标题叫什么不重要，关键是让 agent 少猜。 推荐结构123456789101112131415161718192021222324252627282930313233# AGENTS.md## Project overviewThis is a Hexo blog source repository using the Butterfly theme.## Setup commands- Build: `npm run build`- P...
Agent 工具使用笔记——Codex 篇
Some content in this article was created with AI assistance. Please verify as needed.Codex CLI 是 OpenAI 官方的本地终端 coding agent。它可以在选定目录中读代码、改文件、跑命令。Codex app、IDE extension、CLI、Web/Cloud 是不同入口，这篇只记我主要用的 CLI。 安装和启动官方推荐的 standalone 安装方式是： 1curl -fsSL https://chatgpt.com/codex/install.sh | sh 启动： 1codex 第一次运行会提示登录，可以用 ChatGPT 账号，也可以用 API key。不同 ChatGPT 计划里的 Codex 权益以官方 pricing 页面为准。 Windows 可以直接在 PowerShell 里跑；需要 Linux 原生环境时再用 WSL2。 常用命令123456codexcodex --versioncodex logincodex exec "s...
Agent 工具使用笔记——Claude Code 篇
Some content in this article was created with AI assistance. Please verify as needed.Claude Code 是 Anthropic 官方的终端型 coding agent。它在本地项目目录里运行，可以读代码、改文件、执行命令，也能通过 CLAUDE.md、settings、slash commands、MCP、hooks 这些机制适配项目工作流。 这里先只记官方 Claude Code 的基本用法。第三方 Anthropic-compatible API 的接入放到 API 那篇里。 安装和启动官方快速开始要求 Node.js 18 或更新版本，登录用 Claude.ai 账号或 Anthropic Console 账号。 123npm install -g @anthropic-ai/claude-codecd your-projectclaude 第一次运行 claude 按提示登录即可。我一般在 Git 仓库根目录启动，省得上下文和可写范围混乱。 常用命令123456claudeclau...
Agent 工具使用笔记——API 接入
Some content in this article was created with AI assistance. Please verify as needed.这篇记一下大模型 API 接入。目标不复杂：知道一次请求由哪些东西组成，然后能把 DeepSeek、OpenRouter 这类服务填到各种 AI 软件、编辑器插件、agent 工具或自己的脚本里。 主要参考 DeepSeek 和 OpenRouter 官方文档。示例只保留最小字段，高级参数先不展开。 调用原理最小调用一般绕不开这几项： 1234API format: OpenAI-compatible / Anthropic-compatible / ...Base URL: https://api.example.comAPI key: sk-...Model: provider/model-name 真正发 HTTP 请求时，还会多出这些东西： 123Endpoint: /chat/completionsHeaders: Authorization + Content-TypeBody: model + m...
Agent 工具使用笔记——选择偏好
Some content in this article was created with AI assistance. Please verify as needed.记录一下自己现在使用 AI agent 工具时的判断。这里说的 agent 主要是能读写项目文件、调用终端、使用 MCP / skills / rules 的那类工具，不是普通聊天机器人。 工具形态现在常见形态大概有这么几种： 编辑器插件：比如 GitHub Copilot。侵入小，但上限受插件形态限制。 AI 集成编辑器：比如 Cursor。体验做得完整，但要迁移编辑器和配置体系。 CLI agent：比如 Claude Code、Codex CLI。更贴近真实开发环境，也方便和现有编辑器配合。 GUI / App agent：比如 Codex app。上手简单，但能不能融入本地工作流要看产品设计。 我现在还是更偏向 CLI。主要原因是已经重度使用 VSCode，不想为了 AI 功能迁移整个编辑器；而 CLI 本来就适合配合 Git、终端、项目脚本和现有编辑器。 我觉得让 ID...