Algebruh

Algebruh 把算术等式与不等式同时交给 Z3、cvc5 和 Lean，输出证明、模型、反例以及求解器之间的分歧。其解释域覆盖整数、精确实数、1 - 256 位向量、模运算和 f32/f64；若使用 AI 生成 Lean tactic，最终结果仍须通过 Lean 内核检查。范围目前不含 `<`、`>=` 等序关系，清晰的语法边界让它更像验证工作台，而非泛化数学助手。