 gaojie
|
bb342fc492
|
docs(lean): 新增 HOWTO_PROOF.md — LeJEPA Lean4 证明过程完整指南
Sync to site1 / sync (push) Has been cancelled
内容涵盖：
- 为什么用 Lean4 做数学证明（vs 传统证明）
- 项目结构与文件依赖关系
- axiom vs theorem 核心概念
- 5 个证明文件逐行走读（Hermite/Uniqueness/Approx/Dirichlet/Planning）
- 关键 Mathlib 定理对照表
- 常用证明策略速查表（linarith/nlinarith/ring/field_simp 等）
- 如何添加新定理的完整步骤
- 调试技巧与常见错误解决
|
2026-06-05 17:37:50 +08:00 |
|
|
gaojie
|
c06c167a0c
|
feat(lean): 复现 LeJEPA Lean4 形式化验证，零 sorry 确认
Sync to site1 / sync (push) Has been cancelled
- 新增 JEPA/lejepa-identifiability/lean/README.md
记录完整复现步骤、环境信息与验证状态汇总
Build completed successfully (8032 jobs)，零 sorry 确认
VERIFIED 18 项 / axiomatized 12 项
- .gitignore 新增 **/.lake/ 排除 Lean 构建缓存（~10 GB）
环境：Lean 4.28.0 + Mathlib v4.28.0 + macOS arm64
|
2026-06-05 17:32:16 +08:00 |
|
|
gaojie
|
c66855adfc
|
refactor: 将子模块转为普通目录，移除外部 git 依赖
Sync to site1 / sync (push) Has been cancelled
- 移除 JEPA/lejepa-identifiability 子模块 gitlink
- 移除 research/multiply/MultiPLY 子模块 gitlink
- 删除 .gitmodules（不再有外部 URL 依赖）
- 两个目录内容作为普通文件纳入主仓库追踪
- 删除各自内部 .git 目录，消除嵌套 git 仓库
|
2026-06-05 17:14:01 +08:00 |
|
|
gaojie
|
b70161f4e5
|
feat(JEPA/math): 新增专题 VII & VIII，更新 README 与项目分析
Sync to site1 / sync (push) Has been cancelled
专题 VII — SIGReg 正则化（07_sigreg_regularization.md，760 行）
- 特征函数匹配损失 L_SIG 完整数学推导
- Cramér-Wold 定理证明：切片投影 → 联合高斯
- 切片技巧：256 个随机方向 + 梯形积分（17 节点）
- losses.py:SIGReg 逐行代码解析，张量形状追踪 (V,B,N)→scalar
- vs VICReg 对比：SIGReg 约束全分布，VICReg 仅约束二阶矩
专题 VIII — 线性 ICA：FastICA 与 JADE（08_linear_ica_fastica_jade.md，701 行）
- 盲源分离模型 x=As，非高斯性度量（峰度/负熵/互信息）
- FastICA 不动点迭代推导（三次收敛）
- JADE 四阶累积量张量 + Jacobi 联合对角化（二次收敛）
- Darmois-Skitovich 定理：ICA 可识别性充要条件
- ICA vs LeJEPA 对偶反转：高斯在 ICA 失败，在 LeJEPA 成功
其他变更：
- JEPA/math/README.md：专题表格新增 VII、VIII 行
- project_analysis.md：Session Log 补充 2026-06-05 工作记录
- lejepa-identifiability 子模块：.gitignore 新增 .venv/
|
2026-06-05 17:06:09 +08:00 |
|
|
gaojie
|
c55f47b287
|
Add multiple research papers in PDF format to the repository, including recent works on AI and physics, with file sizes ranging from 1.7 MB to 32.3 MB.
Sync to site1 / sync (push) Has been cancelled
|
2026-06-02 04:12:38 +08:00 |
|