Cover Image

The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Mayeux, Arnaud, Zhang, Jujian
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Artificial Intelligence Algebraic Geometry
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4
by: Mayeux, Arnaud, et al.
Published: (2026)

On multi-graded Proj schemes
by: Mayeux, Arnaud, et al.
Published: (2023)

Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4
by: Huang, Yihe, et al.
Published: (2026)

Topological and scheme-theoretic properties of the $D$-graded Proj construction
by: Goebler, Felix
Published: (2026)

A polyptych of multi-centered deformation spaces
by: Dubouloz, Adrien, et al.
Published: (2024)

Approximating parametric suprema for constructible and power-constructible functions
by: Buggenhout, Tijs, et al.
Published: (2026)

Hologram Reasoning for Solving Algebra Problems with Geometry Diagrams
by: Huang, Litian, et al.
Published: (2024)

Algebraic Magnetism Invariants of Self-Actions of Diagonalizable Monoid Schemes
by: Mayeux, Arnaud
Published: (2025)

Algebraic magnetism invariants of a double scalar action on the projective plane
by: Mayeux, Arnaud
Published: (2025)

Algebraic Magnetism
by: Mayeux, Arnaud
Published: (2022)

Algebraic Magnetism: $X$-products of attractors via $\mathbb{F}_1$-geometry
by: Mayeux, Arnaud
Published: (2026)

Multi-centered dilatations, congruent isomorphisms and Rost double deformation space
by: Mayeux, Arnaud
Published: (2023)

An illustration of formal moduli problems with differential graded Lie algebras
by: Wynner, Ethan Eugene
Published: (2025)

Synthetic Differential Geometry in Lean
by: Brasca, Riccardo, et al.
Published: (2026)

Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems
by: Simmons, William, et al.
Published: (2023)

PBLean: Pseudo-Boolean Proof Certificates for Lean 4
by: Szeider, Stefan
Published: (2026)

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
by: Ospanov, Azim, et al.
Published: (2025)

Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
by: Yin, David, et al.
Published: (2025)

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
by: Shen, Austin, et al.
Published: (2026)

Algebraic Closure of Matrix Sets Recognized by 1-VASS
by: Manssour, Rida Ait El, et al.
Published: (2025)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
by: Song, Peiyang, et al.
Published: (2024)

Proceedings 14th International Conference on Automated Deduction in Geometry
by: Quaresma, Pedro, et al.
Published: (2024)

Nash maps over large fields
by: Walsberg, Erik
Published: (2025)

Large implies henselian
by: Johnson, Will, et al.
Published: (2025)

Linear Logic and the Hilbert Scheme
by: Troiani, William, et al.
Published: (2025)

Hyperbolicity and model-complete fields
by: Szachniewicz, Michał, et al.
Published: (2024)

There is no Definable Grauert Direct Image Theorem
by: Esnault, Hélène, et al.
Published: (2026)

Periods in Families and Derivatives of Period Maps
by: Bakker, Ben, et al.
Published: (2024)

A curve and its abstract generalized Jacobian
by: Castle, Benjamin, et al.
Published: (2026)

A note on the definability of genus for Zariski geometries
by: García, Darío, et al.
Published: (2021)

Curve-excluding fields
by: Johnson, Will, et al.
Published: (2023)

Differentiable approximation of continuous definable maps that preserves the image
by: Carbone, Antonio
Published: (2023)

The Functor of Points Approach to Schemes in Cubical Agda
by: Zeuner, Max, et al.
Published: (2024)

Corrigendum to `Evaluation of motivic functions, non-nullity, and integrability in fibers', Advances in Mathematics, Vol. 409, Part A, Paper No. 108635, 29 pages, doi:10.1016/j.aim.2022.108635 (2022)
by: Cluckers, Raf, et al.
Published: (2026)

Models of Abelian varieties over valued fields, using model theory
by: Halevi, Yatir
Published: (2023)

Univalent Foundations of Constructive Algebraic Geometry
by: Zeuner, Max
Published: (2024)

Factorizing formal contexts from closures of necessity operators
by: Aragón, Roberto G., et al.
Published: (2026)

Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning
by: Bourigault, Pauline, et al.
Published: (2026)

Premise Selection for a Lean Hammer
by: Zhu, Thomas, et al.
Published: (2025)

Progress in Formalizing Sphere Packing in Dimension 8
by: Hariharan, Sidharth, et al.
Published: (2026)