Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with the computational aspects of these. In particular, computing the ring of integers of a given number field is one of the main tasks of computational algebraic number theory. In this paper, we describe a formalization in Lean 4 for certifying such computations. In order to accomplish this, we developed several data types amenable to computation. Moreover, many other underlying mathematical concepts and results had to be formalized, most of which are also of independent interest. These include resultants and discriminants, as well as methods for proving irreducibility of univariate polynomials over finite fields and over the rational numbers. To illustrate the feasibility of our strategy, we formally verified entries from the $\textit{Number fields}$ section of the $\textit{L-functions and modular forms database}$ (LMFDB). These concern, for several number fields, the explicitly given $\textit{integral basis}$ of the ring of integers and the $\textit{discriminant}$. To accomplish this, we wrote SageMath code that computes the corresponding certificates and outputs a Lean proof of the statement to be verified.


翻译:暂无翻译

0
下载
关闭预览

相关内容

牛津大学最新《计算代数拓扑》笔记书,107页pdf
专知会员服务
42+阅读 · 2022年2月17日
专知会员服务
49+阅读 · 2021年6月2日
【ACL2020】多模态信息抽取,365页ppt
专知会员服务
143+阅读 · 2020年7月6日
ExBert — 可视化分析Transformer学到的表示
专知会员服务
31+阅读 · 2019年10月16日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
RL解决'BipedalWalkerHardcore-v2' (SOTA)
CreateAMind
31+阅读 · 2019年7月17日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
利用动态深度学习预测金融时间序列基于Python
量化投资与机器学习
18+阅读 · 2018年10月30日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
条件概率和贝叶斯公式 - 图解概率 03
遇见数学
10+阅读 · 2018年6月5日
概率图模型体系:HMM、MEMM、CRF
机器学习研究会
30+阅读 · 2018年2月10日
CNN 反向传播算法推导
统计学习与视觉计算组
30+阅读 · 2017年12月29日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Layer Normalization原理及其TensorFlow实现
深度学习每日摘要
32+阅读 · 2017年6月17日
基于LDA的主题模型实践(三)
机器学习深度学习实战原创交流
23+阅读 · 2015年10月12日
国家自然科学基金
1+阅读 · 2017年12月31日
国家自然科学基金
1+阅读 · 2017年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Arxiv
0+阅读 · 10月31日
VIP会员
相关资讯
RL解决'BipedalWalkerHardcore-v2' (SOTA)
CreateAMind
31+阅读 · 2019年7月17日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
利用动态深度学习预测金融时间序列基于Python
量化投资与机器学习
18+阅读 · 2018年10月30日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
条件概率和贝叶斯公式 - 图解概率 03
遇见数学
10+阅读 · 2018年6月5日
概率图模型体系:HMM、MEMM、CRF
机器学习研究会
30+阅读 · 2018年2月10日
CNN 反向传播算法推导
统计学习与视觉计算组
30+阅读 · 2017年12月29日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Layer Normalization原理及其TensorFlow实现
深度学习每日摘要
32+阅读 · 2017年6月17日
基于LDA的主题模型实践(三)
机器学习深度学习实战原创交流
23+阅读 · 2015年10月12日
相关基金
国家自然科学基金
1+阅读 · 2017年12月31日
国家自然科学基金
1+阅读 · 2017年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员