算法形式化定理库

人工智能机器人案例ID：235162

Energy

15 年经验· 智慧芽（中国）科技有限公司

微信扫码沟通，客服可协助直接对接工程师；如当前档期不合，也可继续推荐相似案例作者。

案例介绍

项目描述：为摆脱传统/复杂/繁琐的纸笔演算，提高算法研究、数学分析效率，专注于实现形式化机械化数学论证。
项目地址：www.lemma.cn
开源代码：https://github.com/math-proof/lemma/tree/main
项目职责：从2009年起，使用C++、sympy、lean4等语言，着手开发交互式形式化数学认证工具。
初期研习：使用知名符号计算库（sympy、maxima、Mathematica），学习当前主流形式化证明编程语言（Lean、Coq、Isabelle）；独立构建公理化数学论证体系与数学题库；
网站搭建：使用php/node.js作应用后台、vue3作前端框架、Mathjax/Katex作数学公式呈现、CodeMirror作在线IDE，搭建个人网站，支持用户在网站上直接查阅，实现数字化的应用数学及算法原理知识库；
探索应用：实现强化学习原理、旋转位置编码、KMeans聚类收敛性的形式化证明，并将机器证明研究成果应用于自然语言处理技术(pytorch/megatron算子的形式化验证)，并持续探索将大语言模型、强化学习策略的研究方法应用于机器证明、数学机械化的研究。
项目业绩：实现一套公理化数学论证体系，即使用少数数学公理、基本运算法则和已知定理证明所有其他数学定理；并独立搭建出一个涵盖5000余个定理且囊括各数学分支学科的数学题库，用于算法原理、arXiv论文的形式化证明