构建于 Lean 4 + Mathlib
LucidMath
LucidMath 是研究院自建的形式化验证引擎，一套以 Lean 4 与 Mathlib 写就的形式化数学库，其中每一条定理都由证明内核逐行检验。LucidMath 判定一个结论成立，凭据不在权威、同行评议或对作者的信任，而在于：一台机器已从公理出发，将它重新推导了一遍，哪怕错漏一步也会被拒绝。一次成功的构建，本身即是证明。
何以可信
机器检验，而非口头断言
每条命题都归结为一份证明内核所接受的证明，仅依标准数学公理、别无其他。任何隐藏的缺口与多余的公理都会被自动检出，并令构建失败。
诚实的状态分级
一个结论，或是 proved（经内核检验）、或是 axiom-audit（结构一致性的脚手架，明确地并非对哲学的证明）、或是 resolved（曾捕获并修正的真实错误，其反例被永久保留为回归护栏）。三者绝不混为一谈。
一命题，三处对齐，自动校验
每个结论都系于一个稳定标识，串联起它的 Lean 证明、登记条目与著作中的徽章。一旦三者发生偏移，持续集成便会报错。
它能找出真实的错误
LucidMath 已经捕获并修正了若干已发表的错误，其中包括一处信用周期公式与一处经济学不等式，并把每一处都化为有护栏守卫、经内核检验的事实。