Skip to content

Releases: SStarrySSky/Measure

Measure v0.1.0

13 Feb 11:01
@SStarrySSky SStarrySSky
v0.1.0
8602138

Choose a tag to compare

View all tags
Measure v0.1.0 Latest
Latest

Measure v0.1.0 — Physics Formalization Library for Lean 4

Measure is a Lean 4 + Mathlib library for physics formalization. Compile-time verification of dimensional consistency, conservation laws, uncertainty propagation, and theory compatibility.

Measure 是基于 Lean 4 + Mathlib 的物理形式化库。编译即验证：量纲一致性、守恒律、不确定度传播、理论兼容性在编译期自动检查。

Core Features | 核心能力

  • Dimension System | 量纲系统 — 7-component SI dimension vectors with rational exponents (QExp). Compile-time dimensional analysis with zero runtime overhead. / 7 维 SI 量纲向量，有理指数，编译期量纲分析，零运行时开销。
  • Quantity Types | 物理量类型 — ExactQ d for exact quantities, UncertainQ d model for measured quantities with uncertainty models (Gaussian / Affine / Interval). / 精确量与测量量，三种误差模型。
  • PhysReal Bridge | 实数桥接 — PhysReal d wraps Mathlib ℝ for formal proofs, bridged to Quantity for computation. / 连接 Mathlib 形式化证明与浮点计算。
  • Theory Module System | 理论模块系统 — theory blocks with axiom isolation, 4-stage conflict detection, rigor level propagation (strict / approximate / empirical / numerical). / 公理隔离、4 阶段冲突检测、严格度传播。
  • Conservation Checker | 守恒律检查器 — C++ FFI 3-pass static analysis for energy, momentum, charge conservation. / C++ FFI 三遍静态分析。
  • 25 Physics Domains | 25 个物理子领域 — Classical mechanics, electromagnetism, quantum mechanics, relativity, QFT, thermodynamics, condensed matter, and more.
  • Custom Tactics | 自定义策略 — dim_check, conserve, approximate, by_symmetry, limit_of.
  • CODATA 2022 Constants | 物理常量 — SI-exact and measured constants with uncertainties. / SI 精确常量与 CODATA 2022 测量常量。

Stats | 统计

  • 283 theorems, 22 axioms, 0 sorry, 0 warnings
  • 161 Lean files, ~20K lines source + ~2700 lines tests
  • C++ FFI kernel: 9 source files, 60+ extern functions
  • Build: ~2881 jobs | Tests: ~2638 jobs

Installation | 安装

From Source | 源码编译

Add to your lakefile.lean / 在你的 lakefile.lean 中添加：

require measure from git
  "https://github.com/SStarrySSky/Measure" @ "v0.1.0"

Then build / 然后构建：

lake exe cache get   # download precompiled Mathlib / 下载 Mathlib 预编译缓存
lake build

Prebuilt | 预编译版本

Download measure-v0.1.0-prebuilt.tar.gz from this release and extract into your project's .lake/ directory:

下载本 Release 附带的 measure-v0.1.0-prebuilt.tar.gz，解压到项目的 .lake/ 目录：

tar -xzf measure-v0.1.0-prebuilt.tar.gz -C .lake/

Requirements | 环境要求

  • elan (Lean version manager / Lean 版本管理器)
  • Lean 4 v4.28.0-rc1
  • C++17 compiler (g++, clang++, or MSVC)

Quick Example | 快速示例

import Measure.Syntax.Theory
import Measure.Syntax.Tactics
import Measure.Physics.Dimensional
import Measure.Constants

open Measure.Dim
open Measure.Quantity

-- Define a theory with compile-time verification
-- 定义理论，编译时自动验证
theory NewtonianGravity where
  axiom newton2 (m : ExactQ dimMass) (a : ExactQ dimAccel) : ExactQ dimForce
  axiom gravForce (m₁ m₂ : ExactQ dimMass) (r : ExactQ dimLength) : ExactQ dimForce

-- Dimensional consistency proof (verified at compile time)
-- 量纲一致性证明（编译期验证）
theorem force_dim_check : dimForce = Dim.mul dimMass dimAccel := by
  native_decide

-- Use physical constants / 使用物理常量
def earthMass := ExactQ.mk dimMass 5.972e24
def earthRadius := ExactQ.mk dimLength 6.371e6
Assets 3
Loading