HOL Light 快速入门：从安装到证明

HOL Light Tutorial

HOL Light 定理证明器的官方手册虽然详尽，但庞大的前置知识往往让新手望而却步。这篇教程提供了一条更轻松的“快速启动”路径，通过循序渐进的实例，带你迅速掌握系统的基本用法。内容涵盖从 Windows 环境下的 WSL 和 Cygwin 配置，到 OCaml 基础，再到命题逻辑、函数定义、归纳证明等核心概念。无论是验证 RSA 加密算法，还是探索实分析中的导数，你都能在这里找到从理论到实践的完整指南，让形式化验证不再高不可攀。