近日，中科院成都信息技术有限公司承担的“自动推理与数学机械化”项目通过了专家组的验收。 
    该项目在定理机器发现及不等式机器证明的新理论和新方法方面取得了重要进展。其主要创新点为：首次成功地采用数值近似方法得到多项式准确因式分解的高效算法；运用自创的带不等式约束的多项式完全判别系统，自动产生了目前其他方法所不能获得的无量词公式；在胞腔分解中采取了分层处理的策略，提出了相对单纯分解算法，使许多原本做不动的复杂系统能逐步成功地完成分解；创建了既能消去根式又不增加维数的降维算法，全面实现了一大类构造性几何不等式的高效机器证明；对于对称形式的多项式正定性的判定，利用对称形式降维的原理，在短时间就能够完成对某些含104～106个变量的4次对称形式的正定性判定；以Dixon结式为基础，提出了一系列高效率算法，解决了Dixon结式的退化问题。