Imagen de Portada

Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Huang, Yihe, Cui, Sizhe, Wang, Jiaqi, Zhang, Jujian
Formato:	Preprint
Publicado:	2026
Materias:	Combinatorics Logic in Computer Science Algebraic Geometry
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
por: Mayeux, Arnaud, et al.
Publicado: (2025)

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

Grothendieck rings of polytopes and non-archimedean semi-algebraic sets
por: Nicaise, Johannes
Publicado: (2024)

Partitioning Theorems for Sets of Semi-Pfaffian Sets, with Applications
por: Lotz, Martin, et al.
Publicado: (2024)

Serre depth and local cohomology
por: Ficarra, Antonino
Publicado: (2026)

Curve-excluding fields
por: Johnson, Will, et al.
Publicado: (2023)

k-Planar and Fan-Crossing Drawings and Transductions of Embeddable Graphs
por: Hliněný, Petr, et al.
Publicado: (2025)

Happy Ending: An Empty Hexagon in Every Set of 30 Points
por: Heule, Marijn J. H., et al.
Publicado: (2024)

A Formal Proof of R(4,5)=25
por: Gauthier, Thibault, et al.
Publicado: (2024)

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

Nuclei of Normal Rational Curves
por: Gmainer, Johannes, et al.
Publicado: (2013)

Curves in projective space and RSK
por: Lian, Carl, et al.
Publicado: (2025)

Synthetic Differential Geometry in Lean
por: Brasca, Riccardo, et al.
Publicado: (2026)

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

Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
por: Dvorak, Martin, et al.
Publicado: (2025)

Maximal Mumford Curves from Planar Graphs
por: Kummer, Mario, et al.
Publicado: (2024)

Distinct Distances on Pfaffian Curves
por: Natarajan, Abhiram, et al.
Publicado: (2025)

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

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

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
por: Hulak, David B., et al.
Publicado: (2026)

Capturing properties of planar diagrams in Lean proof assistant software
por: Litterick, Alastair, et al.
Publicado: (2025)

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)
por: Cluckers, Raf, et al.
Publicado: (2026)

Formal Verification of the Empty Hexagon Number
por: Subercaseaux, Bernardo, et al.
Publicado: (2024)

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

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

Nash maps over large fields
por: Walsberg, Erik
Publicado: (2025)

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

Large implies henselian
por: Johnson, Will, et al.
Publicado: (2025)

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

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

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

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

Univalent Foundations of Constructive Algebraic Geometry
por: Zeuner, Max
Publicado: (2024)

On geometrically $C_1$ fields
por: Kartas, Konstantinos
Publicado: (2024)

Algebraic curves, rich points, and doubly-ruled surfaces
por: Guth, Larry, et al.
Publicado: (2015)

Indivisibility and uniform computational strength
por: Gill, Kenneth
Publicado: (2023)

Decomposing graphs into stable and ordered parts
por: Buffière, Hector, et al.
Publicado: (2025)

Monadic Second-Order Logic of Permutations
por: Jelínek, Vít, et al.
Publicado: (2025)

Decidability for Sturmian words
por: Hieronymi, Philipp, et al.
Publicado: (2021)

Torus orbit closures and 1-strip-less tableaux
por: Lian, Carl
Publicado: (2023)