开发者用 Lean 4 形式化非对称度规张量论文，174 次提交开源
SubtleGradient · x · 2026-10-30
GitHub 上出现一个名为 asymmetric-tensor 的开源项目，为 Binyamin Tsadik Bair-Mosheh 的论文《The Asymmetric Metric-Tensor and the Thermodynamic Equation of State》构建 Lean 4 研究伴随(formalization companion),将非对称度规张量与热力学状态方程的形式化内容用 Lean 4 证明助手整理成可审计的代码库。仓库包含 ProofAudit.lean 审计文件、连续介质力学、宇宙透镜效应等章节目录，共 174 次提交，采用 Apache-2.0 许可。发帖人称朋友「搞懂了这一切然后写了下来」，自己协助了软件工程部分。展示了用形式化方法辅助独立理论物理研究的做法。
「编程与Agent」频道最新
- 73项服务分拣:MCP工具哪些agent能自助开通,哪些必须人来点 — Total-Reasonable · 2026-10-30
- RL 数据公司的秘密算法：用 Claude 合成测试并迭代改进 Agent — teodorio · 2026-10-30
- 7 个 AI 模型审同一代码库全员虚报完成率，作者复盘任务设计的 7 个错误 — rseroter · 2026-10-30
- Supabase 曾把每分钟数千新数据库误判为 DDoS，实为 Lovable 静默集成 — alifcoder · 2026-10-30
- Graphicle:给编程 Agent 加代码图谱和记忆的开源 Rust 工具 — adnan_hashmi · 2026-10-30
- tiny-llm 开源课:在 Mac 上手搓 vLLM 式推理引擎,修完性能坑才算毕业 — techNmak · 2026-10-30