Imagen de Portada

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Baek, Jineon, Lee, Seewoo
Formato:	Preprint
Publicado:	2024
Materias:	Logic in Computer Science Rings and Algebras
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Formalizing Gröbner Basis Theory in Lean
por: Guo, Junyu, et al.
Publicado: (2026)

Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean
por: del Barco, Viviana, et al.
Publicado: (2025)

Formalizing Wu-Ritt Method in Lean 4
por: Xiao, Yuxuan, et al.
Publicado: (2026)

Local structure of idempotent algebras I
por: Bulatov, Andrei A.
Publicado: (2020)

When Darwin met Ianus: dichotomies of expressivity
por: Brunar, Johanna, et al.
Publicado: (2025)

Automated Tactics for Polynomial Reasoning in Lean 4
por: Shen, Hao, et al.
Publicado: (2026)

Network Satisfaction Problems Solved by k-Consistency
por: Bodirsky, Manuel, et al.
Publicado: (2023)

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4
por: Guan, Naillin, et al.
Publicado: (2025)

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
por: Bolan, Matthew, et al.
Publicado: (2025)

A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
por: Ramos, Arthur F., et al.
Publicado: (2026)

A simplified proof of the CSP Dichotomy Conjecture and XY-symmetric operations
por: Zhuk, Dmitriy
Publicado: (2024)

Symmetric Linear Arc Monadic Datalog and Gadget Reductions
por: Bodirsky, Manuel, et al.
Publicado: (2024)

An algebraic proof of the dichotomy for graph orientation problems with forbidden tournaments
por: Feller, Roman, et al.
Publicado: (2024)

The Network Satisfaction Problem for Relation Algebras with at most 4 Atoms
por: Bodirsky, Manuel, et al.
Publicado: (2025)

Formal conjugacy and asymptotic differential algebra
por: Bagayoko, Vincent
Publicado: (2024)

A Formalization of Divided Powers in Lean
por: Chambert-Loir, Antoine, et al.
Publicado: (2025)

Relational correspondences for L-fuzzy rough approximations defined on De Morgan Heyting algebras
por: Järvinen, Jouni, et al.
Publicado: (2023)

The first fatal axiom for weakened sequential products on finite MV-effect algebras: Local obstruction, exact low-rank classification, and the rank-one boundary case
por: Higuchi, Joaquim Reizi
Publicado: (2026)

Formalizing Automated Market Makers in the Lean 4 Theorem Prover
por: Pusceddu, Daniele, et al.
Publicado: (2024)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
por: Qian, Yicheng, et al.
Publicado: (2025)

Trees and spectra of Heyting algebras
por: Fornasiere, Damiano, et al.
Publicado: (2024)

Almost free modules, perfect decomposition and Enochs's conjecture
por: Cortés-Izurdiaga, Manuel, et al.
Publicado: (2024)

Automorphisms and derivations on algebras endowed with formal infinite sums
por: Bagayoko, Vincent, et al.
Publicado: (2024)

Some applications of finite BL-algebras
por: Flaut, Cristina, et al.
Publicado: (2025)

The theory of implicit operations
por: Carai, Luca, et al.
Publicado: (2025)

Varieties of unary-determined distributive $\ell$-magmas and bunched implication algebras
por: Alpay, Natanael, et al.
Publicado: (2022)

Taylor expansions over generalised power series
por: Bagayoko, Vincent, et al.
Publicado: (2025)

A Module-theoretic Introduction to Abstract Elementary Classes
por: Boney, Will
Publicado: (2025)

Bass modules and embeddings into free modules
por: Pillay, Anand, et al.
Publicado: (2025)

Sharply 2-transitive groups of finite Morley rank
por: Altinel, Tuna, et al.
Publicado: (2018)

Constructive Quantifier Elimination with a Focus on Matrix Rings
por: Illmer, Maximilian, et al.
Publicado: (2025)

An addendum to "The theory of implicit operations"
por: Carai, Luca, et al.
Publicado: (2025)

Cylindric quasi-implication algebras
por: McDonald, Joseph
Publicado: (2025)

Quasicomplemented distributive nearlattices
por: Calomino, Ismael
Publicado: (2025)

Dual Ploščica spaces of ortholattices
por: Craig, Andrew, et al.
Publicado: (2026)

Permutation clones that preserve relations
por: Boykett, Tim
Publicado: (2024)

LeanAgent: Lifelong Learning for Formal Theorem Proving
por: Kumarappan, Adarsh, et al.
Publicado: (2024)

Formalizing CHSH Rigidity in Lean 4
por: Zhao, Tianrun, et al.
Publicado: (2026)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
por: Li, Jinzheng, et al.
Publicado: (2026)

The fork and its role in unification of closure algebras
por: Düntsch, Ivo, et al.
Publicado: (2023)