BaDaaS/cryptography.academy

# 密码学学院 一个用于学习密码学的教育平台，在 Lean 4 中具有形式化基础。 目前处于 Vibe-coded 阶段。只有 `data` 目录中的文件值得查看。 ## 愿景 一本活教材，其中： - 每一个定义都是精确的（Lean 4 代码） - 每一个定理都引用其来源论文 - 证明可以随着时间的推移逐步形式化 - 交互式可视化建立几何直觉 - 每个结果的形式化状态都是透明的 ## 项目结构 ``` . ├── lean/ # Lean 4 formalizations │ └── CryptoAcademy/ │ ├── Meta/ # Infrastructure (papers, status tracking) │ ├── Foundations/ # Mathematical prerequisites │ ├── Primitives/ # Cryptographic building blocks │ └── Proofs/ # Zero-knowledge and arguments ├── web/ # Astro website └── Branding/ # Logos and assets ``` ## 快速开始 ``` # 安装 dependencies make setup # Build everything make build # 启动 development server make serve ``` ## 开发 请参阅网站上的设置页面以获取详细的环境设置。 ### 前置条件 - [elan](https://github.com/leanprover/elan) - Lean 版本管理器 - Node.js 20+ - npm 或 pnpm ### 命令 | 命令 | 描述 | |---------|-------------| | `make help` | 显示所有可用命令 | | `make build` | 构建 Lean 证明和网站 | | `make serve` | 启动开发服务器 | | `make test` | 运行所有测试 | | `make lint` | 运行 linter | | `make format` | 格式化代码 | ## 开发者 **BaDaaS** — 位于比利时的数学研究实验室。 ## 技术栈 ### 形式化证明 - **Lean 4**（最新版本） — 用于编写机器可检查证明的依赖类型编程语言。因其现代语法、快速编译和强大的元编程能力而被选用。 - **Mathlib4** (v4.26.0) — 全面的数学库，提供密码学定义所需的基础代数结构、数论和分析。 ### Web 框架 - **Astro** (5.x) — 具有岛屿架构的静态网站生成器。因其默认零 JS 的方法、卓越的性能以及对 MDX 的一流支持而被选用。非常适合以内容为主的教育网站。 - **React** (18.x) — 用于交互式组件（可视化、代码编辑器）的 UI 库。仅在需要交互性的地方使用，使大多数页面保持为静态 HTML。 - **MDX** (3.x) — 支持 JSX 组件的 Markdown。能够创建混合了散文、数学公式和交互式 React 组件的丰富教育内容。 ### 样式 - **Tailwind CSS** (4.x) — 实用优先的 CSS 框架。因其快速原型设计、一致的设计系统以及无需编写自定义 CSS 即可出色支持暗黑模式而被选用。 ### 图标 - **lucide-react** — 简洁、一致的 UI 图标（导航、按钮、指示器）。采用 MIT 许可，包含 1000 多个图标。 - **@icons-pack/react-simple-icons** — 用于社交链接（GitHub、X/Twitter）的品牌图标。官方 Simple Icons 的 React 组件版本。 ### 开发基础设施 - **Node.js** (24+) — 用于构建工具和开发服务器的 JavaScript 运行时。 - **elan** — Lean 版本管理器，确保不同环境下 Lean 工具链的一致性。 - **Lake** — Lean 的官方构建系统和包管理器。 - **Make** — 标准构建自动化。为 Lean 和 Web 项目提供一致的接口（`make build`、`make serve`、`make test`）。 ### CI/CD - **GitHub Actions** — 持续集成（lint、构建、测试）并部署到 GitHub Pages。 - **Dependabot** — 自动化依赖项更新，每周检查 npm 包和 GitHub Actions。 ### 未来集成 - **lean4web** — 基于浏览器的 Lean 编辑器，用于交互式证明探索，无需本地安装。 - **Postiz** — 用于内容分发的社交媒体自动化（计划中）。 ## 许可证 MIT

标签：Astro, GNU通用公共许可证, Lean 4, Mathlib4, MITM代理, Node.js, Syscall, Web开发, 交互式定理证明, 依赖类型编程, 在线教育, 学术研究, 密码学, 密码学原语, 形式化验证, 手动系统调用, 教科书, 数学基础, 零知识证明