会员服务
形式化 · 呈现 ·
5 月 31 日
Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4
翻译：在Lean4中形式化多分次Brenner-Schröer Proj概形与环的膨胀
Arnaud Mayeux,Jujian Zhang
Arnaud Mayeux,Jujian Zhang

We present a detailed formalization in Lean4 of some multigraded algebraic geometry constructions, focusing on the Brenner--Schröer Proj construction and algebraic dilatations of rings.


翻译：我们呈现了若干多分次代数几何构造在Lean4中的详细形式化，重点聚焦于Brenner–Schröer Proj构造与环的代数膨胀。
0
下载
关闭预览

相关内容

【LoG 2024教程】几何生成模型教程
【LoG 2024教程】几何生成模型教程
专知会员服务
32+阅读 · 2024年11月28日
多模态模型架构的演变
多模态模型架构的演变
专知会员服务
71+阅读 · 2024年5月29日
【ICML2022】Branchformer:并行MLP-Attention架构，捕捉局部和全局上下文，用于语音识别和理解
【ICML2022】Branchformer:并行MLP-Attention架构，捕捉局部和全局上下文，用于语音识别和理解
专知会员服务
25+阅读 · 2022年7月8日
【EPFL-Nicolas Boumal新书】光滑流形优化导论，362页pdf，An introduction to optimization on smooth manifolds
【EPFL-Nicolas Boumal新书】光滑流形优化导论，362页pdf，An introduction to optimization on smooth manifolds
专知会员服务
34+阅读 · 2022年3月4日
Graph Normalization (GN)：为图神经网络学习一个有效的图归一化
Graph Normalization (GN)：为图神经网络学习一个有效的图归一化
专知会员服务
16+阅读 · 2020年9月28日
【ACL2020】Span-ConveRT：预训练对话表示小样本跨度提取，Span-ConveRT: Few-shot Span Extraction for Dialog with Pretrained Conversational Representations
【ACL2020】Span-ConveRT：预训练对话表示小样本跨度提取，Span-ConveRT: Few-shot Span Extraction for Dialog with Pretrained Conversational Representations
专知会员服务
17+阅读 · 2020年5月19日
【DeepMind】PolyGen: 一种三维网格的自回归生成模型，PolyGen: An Autoregressive Generative Model of 3D Meshes
【DeepMind】PolyGen: 一种三维网格的自回归生成模型，PolyGen: An Autoregressive Generative Model of 3D Meshes
专知会员服务
37+阅读 · 2020年2月27日
【ML课程】多变量微积分（Multivariable Calculus），加州大学伯克利分校| Prof. Denis Auroux
【ML课程】多变量微积分（Multivariable Calculus），加州大学伯克利分校| Prof. Denis Auroux
专知会员服务
10+阅读 · 2020年1月7日
【论文】量子知识图嵌入（Quaternion Knowledge Graph Embeddings），罗切斯特大学| Shuai Zhang
【论文】量子知识图嵌入（Quaternion Knowledge Graph Embeddings），罗切斯特大学| Shuai Zhang
专知会员服务
49+阅读 · 2019年12月30日
【论文】多关系庞加莱图嵌入（Multi-relational Poincaré Graph Embeddings），爱丁堡大学| Ivana Balažević
【论文】多关系庞加莱图嵌入（Multi-relational Poincaré Graph Embeddings），爱丁堡大学| Ivana Balažević
专知会员服务
59+阅读 · 2019年12月30日
注意力机制 | 图卷积多跳注意力机制 | Direct multi-hop Attention based GNN
注意力机制 | 图卷积多跳注意力机制 | Direct multi-hop Attention based GNN
AINLP
22+阅读 · 2020年11月29日
系列教程GNN-algorithms之二：《切比雪夫显神威—ChebyNet》
系列教程GNN-algorithms之二：《切比雪夫显神威—ChebyNet》
专知
46+阅读 · 2020年8月4日
(普林斯顿讲义)：高维概率论，326页pdf《Probability in High Dimension》
(普林斯顿讲义)：高维概率论，326页pdf《Probability in High Dimension》
专知
21+阅读 · 2020年5月30日
KG 高引论文解读两篇 | 两种模型：多层卷积神经网络、知识感知路径递归网络
KG 高引论文解读两篇 | 两种模型：多层卷积神经网络、知识感知路径递归网络
学术头条
18+阅读 · 2019年12月8日
【泡泡图灵智库】ContextDesc：用跨模态上下文增强的局部描述子
【泡泡图灵智库】ContextDesc：用跨模态上下文增强的局部描述子
泡泡机器人SLAM
34+阅读 · 2019年9月18日
disentangled-representation-papers
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
全新视角：用变分推断统一理解生成模型（VAE、GAN、AAE、ALI）
全新视角：用变分推断统一理解生成模型（VAE、GAN、AAE、ALI）
PaperWeekly
15+阅读 · 2018年7月19日
【深度学习】深度学习的几何观点：流形分布定律、学习能力的上限、概率变换的几何观点
【深度学习】深度学习的几何观点：流形分布定律、学习能力的上限、概率变换的几何观点
产业智能官
10+阅读 · 2018年6月23日
【论文】变分推断（Variational inference)的总结
【论文】变分推断（Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
图上的归纳表示学习
图上的归纳表示学习
科技创新与创业
23+阅读 · 2017年11月9日
几类平面微分系统的极限环分支
国家自然科学基金
1+阅读 · 2015年12月31日
几类近可积多项式系统和分段光滑系统的极限环分支
国家自然科学基金
0+阅读 · 2015年12月31日
分数次椭圆型方程解的集中现象
国家自然科学基金
0+阅读 · 2015年12月31日
广义欧拉多项式的实根性
国家自然科学基金
0+阅读 · 2015年12月31日
关于 Finsler 流形上调和映射与 Laplacian 的若干问题研究
国家自然科学基金
1+阅读 · 2014年12月31日
与正交多项式相关的几个问题及其研究
国家自然科学基金
0+阅读 · 2014年12月31日
多元多项式环的Hermite性质与多项式矩阵的分解
国家自然科学基金
0+阅读 · 2014年12月31日
套子代数的Hochschild上同调及套的分类
国家自然科学基金
3+阅读 · 2014年12月31日
分形几何中的嵌入问题
国家自然科学基金
0+阅读 · 2014年12月31日
某些分形集上拉普拉斯算子的谱分析及相关问题
国家自然科学基金
0+阅读 · 2014年12月31日
Revisiting average case complexity of multilevel syllogistic: From the 1995 Courant Technical Report to Lean 4 Formalization
Arxiv
0+阅读 · 6月15日
A Lean 4 Formalization of Euclidean Domain Algorithms from a 1986 Icon Experimentation Package
Arxiv
0+阅读 · 6月14日
AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory
Arxiv
0+阅读 · 6月10日
Formalizing Schwartz functions and tempered distributions
Arxiv
0+阅读 · 6月9日
Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4
Arxiv
0+阅读 · 6月8日
A formal proof of the Ramanujan--Nagell theorem in Lean 4
Arxiv
0+阅读 · 6月1日
A Simple Sub-Polynomial Degree Coboundary Expander
Arxiv
0+阅读 · 5月21日
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
Arxiv
0+阅读 · 5月20日
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
Arxiv
0+阅读 · 5月1日
Border subrank of higher order tensors and algebras
Arxiv
0+阅读 · 4月21日
VIP会员
文章信息
前往arXiv
下载PDF
相关主题
形式化
呈现
最新内容
ICML 2026 | FR3D：解耦自车运动的未来动态三维重建世界模型
ICML 2026 | FR3D：解耦自车运动的未来动态三维重建世界模型
专知会员服务
1+阅读 · 今天14:49
【伯克利博士论文】迈向可扩展与自我演进的大语言模型智能体
【伯克利博士论文】迈向可扩展与自我演进的大语言模型智能体
专知会员服务
1+阅读 · 今天14:47
学习数据的几何：形状空间分析数学综述
学习数据的几何：形状空间分析数学综述
专知会员服务
1+阅读 · 今天14:45
《现代防空系统综述：架构、传感器、拦截器及新兴威胁环境对基础设施受限防御环境的影响》2026最新长综述
《现代防空系统综述：架构、传感器、拦截器及新兴威胁环境对基础设施受限防御环境的影响》2026最新长综述
专知会员服务
3+阅读 · 今天14:22
定向能反无人机系统最新发展动态
定向能反无人机系统最新发展动态
专知会员服务
5+阅读 · 今天13:50
从燃煤战舰到算法战争：水面指挥的永恒要求
从燃煤战舰到算法战争：水面指挥的永恒要求
专知会员服务
3+阅读 · 今天13:33
《短程弹道再入飞行器拦截时间中的一项异常现象》
《短程弹道再入飞行器拦截时间中的一项异常现象》
专知会员服务
3+阅读 · 今天13:30
《基于回归方法与任务上下文的对抗环境动态战术网络报文优先级排序》
《基于回归方法与任务上下文的对抗环境动态战术网络报文优先级排序》
专知会员服务
3+阅读 · 今天13:28
美智库《战术级指挥控制的迫切要求：构建弹性机动式指挥控制网络》报告
美智库《战术级指挥控制的迫切要求：构建弹性机动式指挥控制网络》报告
专知会员服务
3+阅读 · 今天13:13
《韩国国防政策与军备出口：韩国安全与国防政策如何塑造其国防工业与军备出口格局》最新100页报告
《韩国国防政策与军备出口：韩国安全与国防政策如何塑造其国防工业与军备出口格局》最新100页报告
专知会员服务
2+阅读 · 今天13:10
ICML 2026 | VOTP：用视频基础模型与最优传输，让离线偏好强化学习只需少量反馈
ICML 2026 | VOTP：用视频基础模型与最优传输，让离线偏好强化学习只需少量反馈
专知会员服务
5+阅读 · 6月16日
多模态代码智能综述：从视觉输入到可执行代码系统
多模态代码智能综述：从视觉输入到可执行代码系统
专知会员服务
7+阅读 · 6月16日
美国马六甲“三重网”概念：安全网、威慑网与杀伤网
美国马六甲“三重网”概念：安全网、威慑网与杀伤网
专知会员服务
5+阅读 · 6月16日
《面向导弹有效发射时机的监督机器学习方法：基于超视距空战仿真》
《面向导弹有效发射时机的监督机器学习方法：基于超视距空战仿真》
专知会员服务
5+阅读 · 6月16日
《通用大语言模型：无人机指挥与控制接口》最新40页
《通用大语言模型：无人机指挥与控制接口》最新40页
专知会员服务
15+阅读 · 6月16日
相关VIP内容
【LoG 2024教程】几何生成模型教程
【LoG 2024教程】几何生成模型教程
专知会员服务
32+阅读 · 2024年11月28日
多模态模型架构的演变
多模态模型架构的演变
专知会员服务
71+阅读 · 2024年5月29日
【ICML2022】Branchformer:并行MLP-Attention架构，捕捉局部和全局上下文，用于语音识别和理解
【ICML2022】Branchformer:并行MLP-Attention架构，捕捉局部和全局上下文，用于语音识别和理解
专知会员服务
25+阅读 · 2022年7月8日
【EPFL-Nicolas Boumal新书】光滑流形优化导论，362页pdf，An introduction to optimization on smooth manifolds
【EPFL-Nicolas Boumal新书】光滑流形优化导论，362页pdf，An introduction to optimization on smooth manifolds
专知会员服务
34+阅读 · 2022年3月4日
Graph Normalization (GN)：为图神经网络学习一个有效的图归一化
Graph Normalization (GN)：为图神经网络学习一个有效的图归一化
专知会员服务
16+阅读 · 2020年9月28日
【ACL2020】Span-ConveRT：预训练对话表示小样本跨度提取，Span-ConveRT: Few-shot Span Extraction for Dialog with Pretrained Conversational Representations
【ACL2020】Span-ConveRT：预训练对话表示小样本跨度提取，Span-ConveRT: Few-shot Span Extraction for Dialog with Pretrained Conversational Representations
专知会员服务
17+阅读 · 2020年5月19日
【DeepMind】PolyGen: 一种三维网格的自回归生成模型，PolyGen: An Autoregressive Generative Model of 3D Meshes
【DeepMind】PolyGen: 一种三维网格的自回归生成模型，PolyGen: An Autoregressive Generative Model of 3D Meshes
专知会员服务
37+阅读 · 2020年2月27日
【ML课程】多变量微积分（Multivariable Calculus），加州大学伯克利分校| Prof. Denis Auroux
【ML课程】多变量微积分（Multivariable Calculus），加州大学伯克利分校| Prof. Denis Auroux
专知会员服务
10+阅读 · 2020年1月7日
【论文】量子知识图嵌入（Quaternion Knowledge Graph Embeddings），罗切斯特大学| Shuai Zhang
【论文】量子知识图嵌入（Quaternion Knowledge Graph Embeddings），罗切斯特大学| Shuai Zhang
专知会员服务
49+阅读 · 2019年12月30日
【论文】多关系庞加莱图嵌入（Multi-relational Poincaré Graph Embeddings），爱丁堡大学| Ivana Balažević
【论文】多关系庞加莱图嵌入（Multi-relational Poincaré Graph Embeddings），爱丁堡大学| Ivana Balažević
专知会员服务
59+阅读 · 2019年12月30日
热门VIP内容
相关资讯
注意力机制 | 图卷积多跳注意力机制 | Direct multi-hop Attention based GNN
注意力机制 | 图卷积多跳注意力机制 | Direct multi-hop Attention based GNN
AINLP
22+阅读 · 2020年11月29日
系列教程GNN-algorithms之二：《切比雪夫显神威—ChebyNet》
系列教程GNN-algorithms之二：《切比雪夫显神威—ChebyNet》
专知
46+阅读 · 2020年8月4日
(普林斯顿讲义)：高维概率论，326页pdf《Probability in High Dimension》
(普林斯顿讲义)：高维概率论，326页pdf《Probability in High Dimension》
专知
21+阅读 · 2020年5月30日
KG 高引论文解读两篇 | 两种模型：多层卷积神经网络、知识感知路径递归网络
KG 高引论文解读两篇 | 两种模型：多层卷积神经网络、知识感知路径递归网络
学术头条
18+阅读 · 2019年12月8日
【泡泡图灵智库】ContextDesc：用跨模态上下文增强的局部描述子
【泡泡图灵智库】ContextDesc：用跨模态上下文增强的局部描述子
泡泡机器人SLAM
34+阅读 · 2019年9月18日
disentangled-representation-papers
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
全新视角：用变分推断统一理解生成模型（VAE、GAN、AAE、ALI）
全新视角：用变分推断统一理解生成模型（VAE、GAN、AAE、ALI）
PaperWeekly
15+阅读 · 2018年7月19日
【深度学习】深度学习的几何观点：流形分布定律、学习能力的上限、概率变换的几何观点
【深度学习】深度学习的几何观点：流形分布定律、学习能力的上限、概率变换的几何观点
产业智能官
10+阅读 · 2018年6月23日
【论文】变分推断（Variational inference)的总结
【论文】变分推断（Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
图上的归纳表示学习
图上的归纳表示学习
科技创新与创业
23+阅读 · 2017年11月9日
相关论文
Revisiting average case complexity of multilevel syllogistic: From the 1995 Courant Technical Report to Lean 4 Formalization
Arxiv
0+阅读 · 6月15日
A Lean 4 Formalization of Euclidean Domain Algorithms from a 1986 Icon Experimentation Package
Arxiv
0+阅读 · 6月14日
AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory
Arxiv
0+阅读 · 6月10日
Formalizing Schwartz functions and tempered distributions
Arxiv
0+阅读 · 6月9日
Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4
Arxiv
0+阅读 · 6月8日
A formal proof of the Ramanujan--Nagell theorem in Lean 4
Arxiv
0+阅读 · 6月1日
A Simple Sub-Polynomial Degree Coboundary Expander
Arxiv
0+阅读 · 5月21日
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
Arxiv
0+阅读 · 5月20日
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
Arxiv
0+阅读 · 5月1日
Border subrank of higher order tensors and algebras
Arxiv
0+阅读 · 4月21日
相关基金
几类平面微分系统的极限环分支
国家自然科学基金
1+阅读 · 2015年12月31日
几类近可积多项式系统和分段光滑系统的极限环分支
国家自然科学基金
0+阅读 · 2015年12月31日
分数次椭圆型方程解的集中现象
国家自然科学基金
0+阅读 · 2015年12月31日
广义欧拉多项式的实根性
国家自然科学基金
0+阅读 · 2015年12月31日
关于 Finsler 流形上调和映射与 Laplacian 的若干问题研究
国家自然科学基金
1+阅读 · 2014年12月31日
与正交多项式相关的几个问题及其研究
国家自然科学基金
0+阅读 · 2014年12月31日
多元多项式环的Hermite性质与多项式矩阵的分解
国家自然科学基金
0+阅读 · 2014年12月31日
套子代数的Hochschild上同调及套的分类
国家自然科学基金
3+阅读 · 2014年12月31日
分形几何中的嵌入问题
国家自然科学基金
0+阅读 · 2014年12月31日
某些分形集上拉普拉斯算子的谱分析及相关问题
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员
Top