We present Generative Logic (GL), a deterministic computer architecture for automated mathematical reasoning. GL starts from axiomatic definitions written in a minimalist Mathematical Programming Language (MPL) and explores a configurable region of their deductive neighborhood. The definitions are compiled into a grid of Logic Blocks (LBs). An LB applies rules by hash-table lookups, and every statement it derives keeps its complete provenance. A run generates conjectures, removes those that counterexamples refute, tries to prove the rest, reduces the proved theorems to an essential core and writes every proof as navigable HTML. An independent verifier checks every proof step. From supplied definitions, GL derives the basic laws of Peano arithmetic and Gauss's summation formula. From previously proved lemmas, further definitions and a supplied list of conjectures, it builds a proof of the Fundamental Theorem of Arithmetic (FTA). These proofs are also exported to Lean 4 and checked by the Lean kernel. The next step is for GL to derive the FTA as well, without supplied conjectures. GL is designed together with a hardware architecture, the Mathematical Processing Unit (MPU).


翻译:暂无翻译

0
下载
关闭预览

相关内容

数学是关于数量、结构、变化等主题的探索。
AAAI 2024 | GCIL:因果视角下的图对比不变学习
专知会员服务
20+阅读 · 2024年3月5日
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
35+阅读 · 2019年10月18日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
61+阅读 · 2019年10月17日
【Code】GraphSAGE 源码解析
AINLP
31+阅读 · 2020年6月22日
预知未来——Gluon 时间序列工具包(GluonTS)
ApacheMXNet
24+阅读 · 2019年6月25日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
论文浅尝 | 用可微的逻辑规则学习完成知识库推理
开放知识图谱
14+阅读 · 2018年7月5日
李宏毅-201806-中文-Deep Reinforcement Learning精品课程分享
深度学习与NLP
15+阅读 · 2018年6月20日
从点到线:逻辑回归到条件随机场
夕小瑶的卖萌屋
15+阅读 · 2017年7月22日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
18+阅读 · 2012年12月31日
Arxiv
0+阅读 · 11月11日
Arxiv
0+阅读 · 10月28日
VIP会员
最新内容
《美空军2026条令文件:对海压制作战》
专知会员服务
23+阅读 · 11月9日
人工智能与战争的未来
专知会员服务
10+阅读 · 11月8日
《Agent Mosaic:识别智能体LLM系统中的机密泄露》
专知会员服务
11+阅读 · 11月8日
人工智能在军事教育中的应用:若干视角与经验
专知会员服务
11+阅读 · 11月6日
“星链”减速与不断适应的乌克兰
专知会员服务
9+阅读 · 11月6日
美国中期选举之后:帕兰提尔面临不确定性?
专知会员服务
6+阅读 · 11月6日
相关VIP内容
AAAI 2024 | GCIL:因果视角下的图对比不变学习
专知会员服务
20+阅读 · 2024年3月5日
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
35+阅读 · 2019年10月18日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
61+阅读 · 2019年10月17日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
18+阅读 · 2012年12月31日
Top
微信扫码咨询专知VIP会员