Image de couverture de livre

Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Mayeux, Arnaud, Zhang, Jujian
Format:	Preprint
Publié:	2026
Sujets:	Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
par: Mayeux, Arnaud, et autres
Publié: (2025)

Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4
par: Huang, Yihe, et autres
Publié: (2026)

On multi-graded Proj schemes
par: Mayeux, Arnaud, et autres
Publié: (2023)

Formalizing CHSH Rigidity in Lean 4
par: Zhao, Tianrun, et autres
Publié: (2026)

Formalizing Wu-Ritt Method in Lean 4
par: Xiao, Yuxuan, et autres
Publié: (2026)

Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
par: Moreira, Walter, et autres
Publié: (2026)

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
par: Baek, Jineon, et autres
Publié: (2024)

Formalizing Automated Market Makers in the Lean 4 Theorem Prover
par: Pusceddu, Daniele, et autres
Publié: (2024)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
par: Qian, Yicheng, et autres
Publié: (2025)

The Chase in Lean -- Crafting a Formal Library for Existential Rule Research
par: Gerlach, Lukas
Publié: (2026)

LeanBET: Formally-verified surface area calculations in Lean
par: Ugwuanyi, Ejike D., et autres
Publié: (2026)

Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids
par: Dvorak, Martin
Publié: (2026)

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
par: Ospanov, Azim, et autres
Publié: (2025)

Formalizing Gröbner Basis Theory in Lean
par: Guo, Junyu, et autres
Publié: (2026)

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
par: Yang, Bowen, et autres
Publié: (2026)

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4
par: Guan, Naillin, et autres
Publié: (2025)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
par: Mohamed, Abdalrhman, et autres
Publié: (2025)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
par: Li, Jinzheng, et autres
Publié: (2026)

LeanAgent: Lifelong Learning for Formal Theorem Proving
par: Kumarappan, Adarsh, et autres
Publié: (2024)

Formalization of physics index notation in Lean 4
par: Tooby-Smith, Joseph
Publié: (2024)

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
par: Santos, Marco Dos, et autres
Publié: (2025)

Formalizing zeta and L-functions in Lean
par: Loeffler, David, et autres
Publié: (2025)

Intuitionistic Propositional Logic in Lean
par: Trufaş, Dafina
Publié: (2024)

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
par: Rowney, Tate, et autres
Publié: (2026)

Lean on Vampire Proofs (Short Paper)
par: Bodingbauer, Jonas, et autres
Publié: (2026)

Process-Driven Autoformalization in Lean 4
par: Lu, Jianqiao, et autres
Publié: (2024)

Automated Tactics for Polynomial Reasoning in Lean 4
par: Shen, Hao, et autres
Publié: (2026)

Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
par: Yanahama, Banri, et autres
Publié: (2026)

Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean
par: del Barco, Viviana, et autres
Publié: (2025)

LeanArchitect: Automating Blueprint Generation for Humans and AI
par: Zhu, Thomas, et autres
Publié: (2026)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
par: Pertseva, Elizaveta, et autres
Publié: (2026)

ZFLean: a framework for set-level mathematics in Lean
par: Trélat, Vincent
Publié: (2026)

PBLean: Pseudo-Boolean Proof Certificates for Lean 4
par: Szeider, Stefan
Publié: (2026)

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
par: Ji, Junye
Publié: (2026)

A unification of graded and substructural logics
par: Hanukaev, Peter, et autres
Publié: (2026)

Extended multi-adjoint logic programming
par: Cornejo, M. Eugenia, et autres
Publié: (2024)

A Formal Proof of R(4,5)=25
par: Gauthier, Thibault, et autres
Publié: (2024)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
par: Zhang, Terry Jingchen, et autres
Publié: (2025)

Syntax and semantics of multi-adjoint normal logic programming
par: Cornejo, M. Eugenia, et autres
Publié: (2024)

Synthetic Differential Geometry in Lean
par: Brasca, Riccardo, et autres
Publié: (2026)