MoonMetamath 0.8.0

MoonMetamath 0.8.0 改进新目标创建和大库定理分页。

• create_goal 新增可选 include_report: true，直接返回创建过程中的实际验证报告。省略或为 false 时保留旧返回结构，公开 MoonBit 签名和 schema 1 不变。
• 网页直接使用这份报告，省去重复 verify；报告异常时保留旧工作并释放候选库，保存恢复继续重新验证。
• 空查询使用定理声明索引，状态从当前声明读取；非空查询及旧 list 保持原语义。
• 新增固定输入、固定预算的 interaction 测量，40 个逐样本摘要随源码与运行包提供，包含初始候选的资源回退。

本机每格三个新进程测量中，set.mm 新目标调用链中位数从 19.30 秒降至 10.98 秒；T7 独立全页收集从 1.53 秒降至 0.187 秒。hol 小库查询没有确定收益。最终 512 MiB verify 对照均完成 48,097 条证明，总耗时增加 12.60%、峰值 RSS 增加 4,264 KiB，均在既定门槛内；这些结果不代表所有机器或浏览器页面耗时。

测量条件和全部样本见 性能记录 与 逐样本数据。

Node 运行包要求 Node.js 24，解压后可直接使用 CLI 与 JSONL stdio。浏览器工作台：https://alexendersokolov.github.io/moonmetamath/web/。

MoonMetamath 0.7.1

MoonMetamath 0.7.1 改进证明错误的位置诊断。

• 普通证明错误定位到对应证明 token；压缩证明的标签表和字符错误定位到对应表项或字符。include 使用子源自己的字节偏移与行列。
• 只在错误发生时重扫当前声明，成功路径不保留逐 token 偏移数组。最终栈错误与声明级交互错误保持原位置语义。
• schema 1、公开 MoonBit 接口、错误码、数学结果和资源预算保持兼容。
• 随包的独立下游示例固定使用 0.7.1；固定空测试文件的获取不再依赖 raw 端点返回空响应。

锁定 set.mm 在 512 MiB old-space、100,000,000 operations 下完成 48,097 条证明验证。资源对照每侧一次，未触及既定停止线；不据此宣称稳定提速。

Node 运行包要求 Node.js 24，解压后可直接使用 CLI 与 JSONL stdio。浏览器工作台：https://alexendersokolov.github.io/moonmetamath/web/。

MoonMetamath 0.7.0

MoonMetamath 0.7.0

新增 shell agent 接入入口：

• theorems 与 rules 文件命令提供分页查询。
• stdio 按 JSONL 顺序处理持续请求，复用数据库与会话，支持错误后检查状态并继续。
• session 错误附带动作索引、成功输入前缀与当前视图。
• 可执行 JavaScript 示例展示结果分支、失败恢复及 finally 资源释放。
• 工作台使用功能名称，API 区分无参考证明评测与解释、审查任务的输入条件。

旧文件命令及 schema 1 保持兼容。程序 ZIP 需要 Node.js 24；协议与资源边界见 docs/CLI.md，发行身份及验证摘要见 release-manifest.json。

MoonMetamath 0.6.0

MoonMetamath 0.6.0

面向 agent 的定理摘要查询、CLI 参数与证明工作台整理。

• 新增 theorems 分页查询，返回标签、目标和验证状态，不包含原证明；旧 list 兼容。
• CLI 支持 --new-label 与 --max-operations，严格检查各命令参数。
• 不交变量对用集合查重，解析展开有操作预算；所有保留源先校验编码与大小。
• 网页统一构造和回放视图刷新，定理面板分页展示，撤下教学引导。
• 整理 API、CLI、开发文档和发行清单，检查解压后的文档链接与实际运行。

源码、工具链、验证范围和资产摘要见随附 release-manifest.json。程序 ZIP 解压后使用 Node.js 24；运行无需 MoonBit 编译器。兼容 schema 1 工作文件。

MoonMetamath 0.5.0 — complete large-database workbench

MoonMetamath 0.5.0

完整 set.mm 工作台已跑通。原 young2d 表达式可创建新目标，完整库上下文中的 wff ph 示例完成了构造、撤回、保存、新 Worker 恢复及导出，浏览器下载文件由官方 C 独立验证。

主要修复是长字符串 JSON 响应的转义分配：按最多4096个UTF-16单元委托原标准库转义，并保护代理对。旧schema1、完整sources及数学执行器保持兼容。浏览器新增明确的默认一千万／大库一亿操作预算，恢复流程沿用当前配置。

本地72项核心测试分别在JS/wasm-gc通过，71项宿主和79项外部样例通过；普通浏览器13项及单独完整大库流程通过，独立审查通过。正式公开验收见Release清单。

附件large-workbench-example.zip含真实下载的工作文件、导出证明及上游许可。导出在本机浏览器观测约82秒，完整流程约3.1分钟；这些是记录环境下的观测。完成的目标为wff ph，不声称发现young2d新证明。

MoonMetamath 0.4.0 — measured real-corpus memory improvements

MoonMetamath 0.4.0

This release establishes reproducible performance baselines on complete pinned hol.mm, nf.mm and set.mm databases, then reduces loading memory without changing the proof executor, public APIs or default limits.

• Avoid the eager source-character array and repeated unchanged scope snapshots.
• Consume private parser tokens by statement after a complete lexical preflight; retain the public scan_source array API and error precedence.
• Scan host includes without a whole-token array and release retained RegExp source text; the actual default CLI now loads set and reports the intended operation-budget limit.
• Add a bounded subprocess benchmark runner, fixed corpus/workload lock, failure records and 46 public sample rows.

On the measured Windows/Node24 system, median process peak RSS fell from 304.62 to 148.55 MiB for nf under the same 512MiB old-space configuration, and from 1908.80 to 749.70 MiB for set under the same 2048MiB/explicit 100m-operation configuration. Set load median fell from 4545 to 3452 ms. Verification itself has no reliable speedup claim; small-file load median increased by about 2.4 ms. Three-sample ranges and all failed cases remain in the report.

The candidate completed all 48,097 set proofs three times with 512 MiB V8 old-space and an explicit 100m-operation budget. Production default 10m operations remains unchanged and reports resource_limit. V8 old-space is not a total-process RSS limit. Full set create_goal/workbench still fails within the tested 512/2048MiB envelope, including a response-parsing OOM; this release does not claim a fully usable large-database workbench.

Validation: 69 core tests on each JS/wasm-gc backend,70 host tests,79 external fixtures and independent reference cases, frozen old notebooks, independent consumers,12 actual Chromium tests, independent proof exports and compiler-free archive execution. Independent measurement and whole-branch reviews found no unresolved issues. Public release verification is recorded in the release manifest after deployment.

No incremental verifier, platform, model experiment or training was added. The product still has no npm runtime dependencies; large upstream corpus bytes and the external C checker are not shipped in the archive.

MoonMetamath 0.3.0 — long-running proof engine foundation

MoonMetamath 0.3.0

This release makes the existing MoonBit proof engine suitable for long-running consumers while preserving schema 1, the legacy dispatcher and the native core interfaces.

• Independent native Engine instances and JavaScript create_dispatcher factories.
• close_session and unload_database with ownership checks, explicit busy errors and stale-handle rejection.
• Earlier verification evidence on immutable databases survives bounded rechecks; each verification report still describes its own attempt.
• Atomic target, new-goal, upload and restore transitions; cancellation cannot revive stale work, and worker failures remain visible.
• Frozen 0.2.0 notebook compatibility fixtures and actual Chromium regression tests, with browser evidence tied to tested assets and independent verification of downloaded proofs.
• A complete standalone MoonBit downstream example using only the root public API, including 80 session-reuse cycles and independently checked exports on JS and wasm-gc.

Validation: 61 core tests on each backend, 47 host tests, 79 fixed external cases, 12 Chromium tests, fresh consumers, independent official C verification and compiler-free ZIP execution. Public CI, registry and download receipts are recorded in the release manifest and project progress after verification.

The Node24 archive runs without a MoonBit compiler, Python, C checker or model credentials. Development browser tests use a pinned Playwright dependency; the product has no npm runtime dependencies.

No new model experiment or full set.mm capacity claim is included. The downstream module is a reproducible integration example, not evidence of external adoption.

MoonMetamath 0.2.0 — proof workbench and bounded real AI completion

MoonMetamath 0.2 adds rule search, atomic step previews, inherited-context new goals, validated saved-work replay and three progressive exercises to the native MoonBit checker.

Browser lab · Mooncakes · Exact-source Windows/Linux CI and Pages

Install moon add AlexenderSokolov/moonmetamath@0.2.0. The Node24 ZIP runs the CLI without a compiler. The optional AI experiment runs from source with the independent C checker.

Validated:55 core tests on each backend,39 host tests,79 upstream expectations,15-operation registry consumers on both backends, real local/public browser flows and independently checked downloaded proof. Seven official-C boundary differences remain documented. Narrow390px and storage-denial branches were not live tested.

The first real AI run completed ten fixed self-authored incomplete exercises:10 completed policy calls and10 independently C-verified model proofs; bounded BFS8/10 with2 budget exhaustions. No original proof, raw source, baseline answer or unrestricted tools were given to the model. Budgets differ:the40-step identity solution exceeds the BFS depth12 cap. This is functional integration evidence, not a standardized benchmark, superiority claim or new mathematics. Actual methods and results.

The experiment ZIP retains all safe observations/actions, task inputs,18 successful proofs and independent C stdout. Credentials and raw machine-path warnings are excluded. Requested model:gpt-6.1-sol low via official Codex ChatGPT authentication; backend model and dollar cost are not exposed. Reported input/output tokens:203344/1110.

Source:97190c31f48c031600d9e5d24cc89851d8c768be. Registry upload preceded publication-doc refinements; all30 MoonBit implementation/interface files were compared byte-for-byte with this release and match. SHA256SUMS identifies the tested runtime ZIP. Organizer decisions, external human adoption and full set.mm performance remain separate unverified outcomes.

MoonMetamath 0.1.1 — IO error classification fixes

Maintenance release fixing filesystem error classification. Missing source roots and unavailable export directories now return HOST_IO / exit3. Exclusive export creation and all mathematical semantics are preserved.

Validation:47 core tests on JS/wasm-gc,15 host tests,79 upstream fixtures; fresh public API consumer and compiler-free archive tests. Windows/Linux CI and Pages: https://github.com/AlexenderSokolov/moonmetamath/actions/runs/39978600841 . Source3ef0942963c01e28ffd5f51d89b8ebb37230ab0c.

Download the Node24 ZIP and run node bin/moonmetamath.mjs --help. No compiler or model is required. Mooncakes: moon add AlexenderSokolov/moonmetamath@0.1.1 .

0.2 work and a genuine AI completion experiment are separately in progress; this patch does not claim those features.

MoonMetamath 0.1.0 — native proof verification and interactive lab

MoonMetamath 0.1.0 brings native MoonBit Metamath verification, checked forward proof construction, a Node CLI and a browser proof lab.

• Try the public proof lab
• Install the Mooncakes module: moon add AlexenderSokolov/moonmetamath@0.1.0
• Download the Node24 ZIP, extract it, then run node bin/moonmetamath.mjs --help. No compiler, npm packages, Python, C verifier or model credentials are needed to use the CLI.

Validation: 47 core tests on JS and wasm-gc; 14 host integration tests; 79 pinned upstream fixtures match expected outcomes and independent mmreference; four official small databases pass the independent official C checker. Both local and public browser construction produced downloaded proofs accepted by the independent C checker. A fresh registry consumer executes load, verify, start, apply, finish and export on both backends. The ZIP is unpacked and exercised without a compiler, including session export and re-verification.

Exact-source Windows/Linux CI and Pages deployment
Source commit: 1029f1d

Limits: full set.mm performance is unmeasured; compressed replay is read-only; ordinary export is limited to completed forward construction. No LLM call, external human adoption or new mathematical theorem is claimed. The official C checker has seven documented boundary-case differences from the fixture expectations; see docs/COMPATIBILITY.md. Peano fixtures with conflicting license headers are not distributed. Contest application and organizer decisions are separate from this technical release.

The ZIP includes retained MIT/Apache/CC0 notices. Source is MIT with documented third-party exceptions. SHA256SUMS.txt identifies this exact release archive.

Post-release acceptance tooling: use main at 4af2f94 or later to run publication rechecks from Windows. The helper now compares public bytes with the exact CI Linux Pages artifact, accounting for platform-specific numeric literal formatting without normalizing source. The v0.1.0 product tag and tested ZIP are unchanged. The updated main also passed Windows/Linux CI and Pages deployment: https://github.com/AlexenderSokolov/moonmetamath/actions/runs/39973540119 . Public deployed-asset SHA256 values are retained in public-assets.json.