标签
Antimony 是一款实验性 CAD 工具，通过在有向无环图（DAG）中连接可脚本化的节点来进行实体建模，使用函数表示来实现构造实体几何（CSG）和由 Python 定义的形状。它支持自动传播更改、交互式视口编辑，以及带特征检测的 STL/高度图导出。
一个在 Lean 4 中实现的形式化验证的3D网格交集算法，只需审查93行规范，信任 Lean 检查器而非1000多行AI生成的代码。它展示了一种减少人工审查工作同时确保正确性的新颖方法。